Proof
01. 1 ⊢ set x ∧ set y, hypo.
02. 1 ⊢ set x, conj_eliml 1.
03. 1 ⊢ set y, conj_elimr 1.
04. ⊢ ⋂(x, y) = ⋂(x, y), eq_refl.
05. ⊢ (x, y) = {{x}, {x, y}}, pair_eq.
06. ⊢ ⋂(x, y) = ⋂{{x}, {x, y}}, eq_subst 5 4, P u ↔ ⋂(x, y) = ⋂u.
07. 1 ⊢ set {x}, set_sg 2.
08. 1 ⊢ set {x, y}, pairing 2 3.
09. 1 ⊢ set {x} ∧ set {x, y}, conj_intro 7 8.
10. 1 ⊢ ⋂{{x}, {x, y}} = {x} ∩ {x, y}, Intersection_pair_set 9.
11. 1 ⊢ ⋂(x, y) = {x} ∩ {x, y}, eq_trans 6 10.
12. ⊢ {x} ⊆ {x, y}, union_incl_left.
13. ⊢ {x} ∩ {x, y} = {x}, intersection_from_incl 12.
14. 1 ⊢ ⋂(x, y) = {x}, eq_trans 11 13.
15. 1 ⊢ ⋂⋂(x, y) = ⋂{x}, f_equal 14, f u = ⋂u.
16. 1 ⊢ ⋂{x} = x, Intersection_sg 2.
17. 1 ⊢ ⋂⋂(x, y) = x, eq_trans 15 16.
18. ⊢ fst (x, y) = ⋂⋂(x, y), fst_eq.
19. 1 ⊢ fst (x, y) = x, eq_trans 18 17.
pair_fst_conj. ⊢ set x ∧ set y → fst (x, y) = x, subj_intro 19.
20. ⊢ ⋃(x, y) = ⋃(x, y), eq_refl.
21. ⊢ ⋃(x, y) = ⋃{{x}, {x, y}}, eq_subst 5 20, P u ↔ ⋃(x, y) = ⋃u.
22. 1 ⊢ ⋃{{x}, {x, y}} = {x} ∪ {x, y}, Union_pair_set 9.
23. 1 ⊢ ⋃(x, y) = {x} ∪ {x, y}, eq_trans 21 22.
24. ⊢ {x} ∪ {x, y} = {x, y}, union_from_incl 12.
25. 1 ⊢ ⋃(x, y) = {x, y}, eq_trans 23 24.
26. 1 ⊢ ⋃⋃(x, y) = ⋃{x, y}, f_equal 25, f u = ⋃u.
27. 1 ⊢ ⋃{x, y} = x ∪ y, Union_pair_set 1.
28. 1 ⊢ ⋃⋃(x, y) = x ∪ y, eq_trans 26 27.
29. 1 ⊢ ⋂{x, y} = x ∩ y, Intersection_pair_set 1.
30. 1 ⊢ ⋂⋃(x, y) = ⋂{x, y}, f_equal 25, f u = ⋂u.
31. 1 ⊢ ⋂⋃(x, y) = x ∩ y, eq_trans 30 29.
32. ⊢ scd (x, y) = ⋂⋃(x, y) ∪ (⋃⋃(x, y) \ ⋂⋂(x, y)), scd_eq.
33. 1 ⊢ scd (x, y) = (x ∩ y) ∪ (⋃⋃(x, y) \ ⋂⋂(x, y)),
eq_subst 31 32, P a ↔ scd (x, y) = a ∪ (⋃⋃(x, y) \ ⋂⋂(x, y)).
34. 1 ⊢ scd (x, y) = (x ∩ y) ∪ ((x ∪ y) \ ⋂⋂(x, y)),
eq_subst 28 33, P a ↔ scd (x, y) = (x ∩ y) ∪ (a \ ⋂⋂(x, y)).
35. 1 ⊢ scd (x, y) = (x ∩ y) ∪ ((x ∪ y) \ x),
eq_subst 17 34, P a ↔ scd (x, y) = (x ∩ y) ∪ ((x ∪ y) \ a).
36. ⊢ (x ∪ y) \ x = (x ∪ y) ∩ compl x, diff_as_inter.
37. 1 ⊢ scd (x, y) = (x ∩ y) ∪ ((x ∪ y) ∩ compl x),
eq_subst 36 35, P a ↔ scd (x, y) = (x ∩ y) ∪ a.
38. ⊢ (x ∪ y) ∩ compl x = (x ∩ compl x) ∪ (y ∩ compl x),
intersection_distr.
39. ⊢ x ∩ compl x = ∅, intersection_compl.
40. ⊢ (x ∩ compl x) ∪ (y ∩ compl x) = ∅ ∪ (y ∩ compl x),
f_equal 39, f a = a ∪ (y ∩ compl x).
41. ⊢ ∅ ∪ (y ∩ compl x) = y ∩ compl x, union_neutl.
42. ⊢ (x ∩ compl x) ∪ (y ∩ compl x) = y ∩ compl x, eq_trans 40 41.
43. ⊢ (x ∪ y) ∩ compl x = y ∩ compl x, eq_trans 38 42.
44. ⊢ y ∩ compl x = compl x ∩ y, intersection_comm.
45. ⊢ (x ∪ y) ∩ compl x = compl x ∩ y, eq_trans 43 44.
46. 1 ⊢ scd (x, y) = (x ∩ y) ∪ (compl x ∩ y),
eq_subst 45 37, P a ↔ scd (x, y) = (x ∩ y) ∪ a.
47. ⊢ (x ∪ compl x) ∩ y = (x ∩ y) ∪ (compl x ∩ y), intersection_distr.
48. ⊢ (x ∩ y) ∪ (compl x ∩ y) = (x ∪ compl x) ∩ y, eq_symm 47.
49. 1 ⊢ scd (x, y) = (x ∪ compl x) ∩ y, eq_trans 46 48.
50. ⊢ x ∪ compl x = UnivCl, union_compl.
51. ⊢ (x ∪ compl x) ∩ y = UnivCl ∩ y, f_equal 50, f a = a ∩ y.
52. ⊢ UnivCl ∩ y = y, intersection_neutl.
53. ⊢ (x ∪ compl x) ∩ y = y, eq_trans 51 52.
54. 1 ⊢ scd (x, y) = y, eq_trans 49 53.
pair_scd_conj. ⊢ set x ∧ set y → scd (x, y) = y, subj_intro 54.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing.