MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  disjxiun Structured version   Visualization version   GIF version

Theorem disjxiun 4920
Description: An indexed union of a disjoint collection of disjoint collections is disjoint if each component is disjoint, and the disjoint unions in the collection are also disjoint. Note that 𝐵(𝑦) and 𝐶(𝑥) may have the displayed free variables. (Contributed by Mario Carneiro, 14-Nov-2016.) (Proof shortened by JJ, 27-May-2021.)
Assertion
Ref Expression
disjxiun (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶 ↔ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵   𝑦,𝐶
Allowed substitution hints:   𝐵(𝑦)   𝐶(𝑥)

Proof of Theorem disjxiun
Dummy variables 𝑠 𝑟 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfiu1 4817 . . . . . 6 𝑦 𝑦𝐴 𝐵
2 nfcv 2926 . . . . . 6 𝑦𝐶
31, 2nfdisj 4903 . . . . 5 𝑦Disj 𝑥 𝑦𝐴 𝐵𝐶
4 disjss1 4897 . . . . . 6 (𝐵 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶Disj 𝑥𝐵 𝐶))
5 ssiun2 4831 . . . . . 6 (𝑦𝐴𝐵 𝑦𝐴 𝐵)
64, 5syl11 33 . . . . 5 (Disj 𝑥 𝑦𝐴 𝐵𝐶 → (𝑦𝐴Disj 𝑥𝐵 𝐶))
73, 6ralrimi 3160 . . . 4 (Disj 𝑥 𝑦𝐴 𝐵𝐶 → ∀𝑦𝐴 Disj 𝑥𝐵 𝐶)
87a1i 11 . . 3 (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶 → ∀𝑦𝐴 Disj 𝑥𝐵 𝐶))
9 simplr 756 . . . . . . . . . 10 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → Disj 𝑥 𝑦𝐴 𝐵𝐶)
10 ssiun2 4831 . . . . . . . . . . . . 13 (𝑢𝐴𝑢 / 𝑦𝐵 𝑢𝐴 𝑢 / 𝑦𝐵)
11 nfcv 2926 . . . . . . . . . . . . . 14 𝑢𝐵
12 nfcsb1v 3800 . . . . . . . . . . . . . 14 𝑦𝑢 / 𝑦𝐵
13 csbeq1a 3791 . . . . . . . . . . . . . 14 (𝑦 = 𝑢𝐵 = 𝑢 / 𝑦𝐵)
1411, 12, 13cbviun 4825 . . . . . . . . . . . . 13 𝑦𝐴 𝐵 = 𝑢𝐴 𝑢 / 𝑦𝐵
1510, 14syl6sseqr 3904 . . . . . . . . . . . 12 (𝑢𝐴𝑢 / 𝑦𝐵 𝑦𝐴 𝐵)
1615adantr 473 . . . . . . . . . . 11 ((𝑢𝐴𝑣𝐴) → 𝑢 / 𝑦𝐵 𝑦𝐴 𝐵)
1716ad2antrl 715 . . . . . . . . . 10 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 / 𝑦𝐵 𝑦𝐴 𝐵)
18 csbeq1 3785 . . . . . . . . . . . . . 14 (𝑢 = 𝑣𝑢 / 𝑦𝐵 = 𝑣 / 𝑦𝐵)
1918sseq1d 3884 . . . . . . . . . . . . 13 (𝑢 = 𝑣 → (𝑢 / 𝑦𝐵 𝑦𝐴 𝐵𝑣 / 𝑦𝐵 𝑦𝐴 𝐵))
2019, 15vtoclga 3487 . . . . . . . . . . . 12 (𝑣𝐴𝑣 / 𝑦𝐵 𝑦𝐴 𝐵)
2120adantl 474 . . . . . . . . . . 11 ((𝑢𝐴𝑣𝐴) → 𝑣 / 𝑦𝐵 𝑦𝐴 𝐵)
2221ad2antrl 715 . . . . . . . . . 10 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 / 𝑦𝐵 𝑦𝐴 𝐵)
2311, 12, 13cbvdisj 4901 . . . . . . . . . . . . . . . 16 (Disj 𝑦𝐴 𝐵Disj 𝑢𝐴 𝑢 / 𝑦𝐵)
2418disjor 4905 . . . . . . . . . . . . . . . 16 (Disj 𝑢𝐴 𝑢 / 𝑦𝐵 ↔ ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅))
2523, 24sylbb 211 . . . . . . . . . . . . . . 15 (Disj 𝑦𝐴 𝐵 → ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅))
26 rsp2 3157 . . . . . . . . . . . . . . 15 (∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅) → ((𝑢𝐴𝑣𝐴) → (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)))
2725, 26syl 17 . . . . . . . . . . . . . 14 (Disj 𝑦𝐴 𝐵 → ((𝑢𝐴𝑣𝐴) → (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)))
2827imp 398 . . . . . . . . . . . . 13 ((Disj 𝑦𝐴 𝐵 ∧ (𝑢𝐴𝑣𝐴)) → (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅))
2928ord 850 . . . . . . . . . . . 12 ((Disj 𝑦𝐴 𝐵 ∧ (𝑢𝐴𝑣𝐴)) → (¬ 𝑢 = 𝑣 → (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅))
3029impr 447 . . . . . . . . . . 11 ((Disj 𝑦𝐴 𝐵 ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)
3130adantlr 702 . . . . . . . . . 10 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)
32 disjiun 4911 . . . . . . . . . 10 ((Disj 𝑥 𝑦𝐴 𝐵𝐶 ∧ (𝑢 / 𝑦𝐵 𝑦𝐴 𝐵𝑣 / 𝑦𝐵 𝑦𝐴 𝐵 ∧ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)) → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅)
339, 17, 22, 31, 32syl13anc 1352 . . . . . . . . 9 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅)
3433expr 449 . . . . . . . 8 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ (𝑢𝐴𝑣𝐴)) → (¬ 𝑢 = 𝑣 → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅))
3534orrd 849 . . . . . . 7 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ (𝑢𝐴𝑣𝐴)) → (𝑢 = 𝑣 ∨ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅))
3635ralrimivva 3135 . . . . . 6 ((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) → ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅))
3718iuneq1d 4812 . . . . . . 7 (𝑢 = 𝑣 𝑥 𝑢 / 𝑦𝐵𝐶 = 𝑥 𝑣 / 𝑦𝐵𝐶)
3837disjor 4905 . . . . . 6 (Disj 𝑢𝐴 𝑥 𝑢 / 𝑦𝐵𝐶 ↔ ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅))
3936, 38sylibr 226 . . . . 5 ((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) → Disj 𝑢𝐴 𝑥 𝑢 / 𝑦𝐵𝐶)
40 nfcv 2926 . . . . . 6 𝑢 𝑥𝐵 𝐶
4112, 2nfiun 4815 . . . . . 6 𝑦 𝑥 𝑢 / 𝑦𝐵𝐶
4213iuneq1d 4812 . . . . . 6 (𝑦 = 𝑢 𝑥𝐵 𝐶 = 𝑥 𝑢 / 𝑦𝐵𝐶)
4340, 41, 42cbvdisj 4901 . . . . 5 (Disj 𝑦𝐴 𝑥𝐵 𝐶Disj 𝑢𝐴 𝑥 𝑢 / 𝑦𝐵𝐶)
4439, 43sylibr 226 . . . 4 ((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) → Disj 𝑦𝐴 𝑥𝐵 𝐶)
4544ex 405 . . 3 (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶))
468, 45jcad 505 . 2 (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶 → (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)))
4714eleq2i 2851 . . . . . . . 8 (𝑟 𝑦𝐴 𝐵𝑟 𝑢𝐴 𝑢 / 𝑦𝐵)
48 eliun 4790 . . . . . . . 8 (𝑟 𝑢𝐴 𝑢 / 𝑦𝐵 ↔ ∃𝑢𝐴 𝑟𝑢 / 𝑦𝐵)
4947, 48bitri 267 . . . . . . 7 (𝑟 𝑦𝐴 𝐵 ↔ ∃𝑢𝐴 𝑟𝑢 / 𝑦𝐵)
50 nfcv 2926 . . . . . . . . . 10 𝑣𝐵
51 nfcsb1v 3800 . . . . . . . . . 10 𝑦𝑣 / 𝑦𝐵
52 csbeq1a 3791 . . . . . . . . . 10 (𝑦 = 𝑣𝐵 = 𝑣 / 𝑦𝐵)
5350, 51, 52cbviun 4825 . . . . . . . . 9 𝑦𝐴 𝐵 = 𝑣𝐴 𝑣 / 𝑦𝐵
5453eleq2i 2851 . . . . . . . 8 (𝑠 𝑦𝐴 𝐵𝑠 𝑣𝐴 𝑣 / 𝑦𝐵)
55 eliun 4790 . . . . . . . 8 (𝑠 𝑣𝐴 𝑣 / 𝑦𝐵 ↔ ∃𝑣𝐴 𝑠𝑣 / 𝑦𝐵)
5654, 55bitri 267 . . . . . . 7 (𝑠 𝑦𝐴 𝐵 ↔ ∃𝑣𝐴 𝑠𝑣 / 𝑦𝐵)
5749, 56anbi12i 617 . . . . . 6 ((𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵) ↔ (∃𝑢𝐴 𝑟𝑢 / 𝑦𝐵 ∧ ∃𝑣𝐴 𝑠𝑣 / 𝑦𝐵))
58 reeanv 3302 . . . . . 6 (∃𝑢𝐴𝑣𝐴 (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ↔ (∃𝑢𝐴 𝑟𝑢 / 𝑦𝐵 ∧ ∃𝑣𝐴 𝑠𝑣 / 𝑦𝐵))
5957, 58bitr4i 270 . . . . 5 ((𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵) ↔ ∃𝑢𝐴𝑣𝐴 (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵))
60 simplrr 765 . . . . . . . . . . 11 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → ¬ 𝑟 = 𝑠)
6112, 2nfdisj 4903 . . . . . . . . . . . . . . . . . . 19 𝑦Disj 𝑥 𝑢 / 𝑦𝐵𝐶
6213disjeq1d 4899 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑢 → (Disj 𝑥𝐵 𝐶Disj 𝑥 𝑢 / 𝑦𝐵𝐶))
6361, 62rspc 3523 . . . . . . . . . . . . . . . . . 18 (𝑢𝐴 → (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑥 𝑢 / 𝑦𝐵𝐶))
6463impcom 399 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝐴 Disj 𝑥𝐵 𝐶𝑢𝐴) → Disj 𝑥 𝑢 / 𝑦𝐵𝐶)
65 disjors 4906 . . . . . . . . . . . . . . . . 17 (Disj 𝑥 𝑢 / 𝑦𝐵𝐶 ↔ ∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
6664, 65sylib 210 . . . . . . . . . . . . . . . 16 ((∀𝑦𝐴 Disj 𝑥𝐵 𝐶𝑢𝐴) → ∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
6766ad2ant2r 734 . . . . . . . . . . . . . . 15 (((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) → ∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
6867adantr 473 . . . . . . . . . . . . . 14 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) → ∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
69 simplrl 764 . . . . . . . . . . . . . . 15 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) ∧ 𝑢 = 𝑣) → 𝑟𝑢 / 𝑦𝐵)
70 simplrr 765 . . . . . . . . . . . . . . . 16 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) ∧ 𝑢 = 𝑣) → 𝑠𝑣 / 𝑦𝐵)
7118adantl 474 . . . . . . . . . . . . . . . 16 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) ∧ 𝑢 = 𝑣) → 𝑢 / 𝑦𝐵 = 𝑣 / 𝑦𝐵)
7270, 71eleqtrrd 2863 . . . . . . . . . . . . . . 15 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) ∧ 𝑢 = 𝑣) → 𝑠𝑢 / 𝑦𝐵)
7369, 72jca 504 . . . . . . . . . . . . . 14 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) ∧ 𝑢 = 𝑣) → (𝑟𝑢 / 𝑦𝐵𝑠𝑢 / 𝑦𝐵))
74 rsp2 3157 . . . . . . . . . . . . . . 15 (∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅) → ((𝑟𝑢 / 𝑦𝐵𝑠𝑢 / 𝑦𝐵) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)))
7574imp 398 . . . . . . . . . . . . . 14 ((∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑢 / 𝑦𝐵)) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
7668, 73, 75syl2an2r 672 . . . . . . . . . . . . 13 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
7776adantlrr 708 . . . . . . . . . . . 12 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
7877ord 850 . . . . . . . . . . 11 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (¬ 𝑟 = 𝑠 → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
7960, 78mpd 15 . . . . . . . . . 10 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)
80 ssiun2 4831 . . . . . . . . . . . . . 14 (𝑟𝑢 / 𝑦𝐵𝑟 / 𝑥𝐶 𝑟 𝑢 / 𝑦𝐵𝑟 / 𝑥𝐶)
81 nfcv 2926 . . . . . . . . . . . . . . 15 𝑟𝐶
82 nfcsb1v 3800 . . . . . . . . . . . . . . 15 𝑥𝑟 / 𝑥𝐶
83 csbeq1a 3791 . . . . . . . . . . . . . . 15 (𝑥 = 𝑟𝐶 = 𝑟 / 𝑥𝐶)
8481, 82, 83cbviun 4825 . . . . . . . . . . . . . 14 𝑥 𝑢 / 𝑦𝐵𝐶 = 𝑟 𝑢 / 𝑦𝐵𝑟 / 𝑥𝐶
8580, 84syl6sseqr 3904 . . . . . . . . . . . . 13 (𝑟𝑢 / 𝑦𝐵𝑟 / 𝑥𝐶 𝑥 𝑢 / 𝑦𝐵𝐶)
86 ssiun2 4831 . . . . . . . . . . . . . 14 (𝑠𝑣 / 𝑦𝐵𝑠 / 𝑥𝐶 𝑠 𝑣 / 𝑦𝐵𝑠 / 𝑥𝐶)
87 nfcv 2926 . . . . . . . . . . . . . . 15 𝑠𝐶
88 nfcsb1v 3800 . . . . . . . . . . . . . . 15 𝑥𝑠 / 𝑥𝐶
89 csbeq1a 3791 . . . . . . . . . . . . . . 15 (𝑥 = 𝑠𝐶 = 𝑠 / 𝑥𝐶)
9087, 88, 89cbviun 4825 . . . . . . . . . . . . . 14 𝑥 𝑣 / 𝑦𝐵𝐶 = 𝑠 𝑣 / 𝑦𝐵𝑠 / 𝑥𝐶
9186, 90syl6sseqr 3904 . . . . . . . . . . . . 13 (𝑠𝑣 / 𝑦𝐵𝑠 / 𝑥𝐶 𝑥 𝑣 / 𝑦𝐵𝐶)
92 ss2in 4095 . . . . . . . . . . . . 13 ((𝑟 / 𝑥𝐶 𝑥 𝑢 / 𝑦𝐵𝐶𝑠 / 𝑥𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) ⊆ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶))
9385, 91, 92syl2an 586 . . . . . . . . . . . 12 ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) ⊆ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶))
9493ad2antrl 715 . . . . . . . . . . 11 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) ⊆ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶))
95 nfcv 2926 . . . . . . . . . . . . . . 15 𝑧 𝑥𝐵 𝐶
96 nfcsb1v 3800 . . . . . . . . . . . . . . . 16 𝑦𝑧 / 𝑦𝐵
9796, 2nfiun 4815 . . . . . . . . . . . . . . 15 𝑦 𝑥 𝑧 / 𝑦𝐵𝐶
98 csbeq1a 3791 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧𝐵 = 𝑧 / 𝑦𝐵)
9998iuneq1d 4812 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 𝑥𝐵 𝐶 = 𝑥 𝑧 / 𝑦𝐵𝐶)
10095, 97, 99cbvdisj 4901 . . . . . . . . . . . . . 14 (Disj 𝑦𝐴 𝑥𝐵 𝐶Disj 𝑧𝐴 𝑥 𝑧 / 𝑦𝐵𝐶)
101100biimpi 208 . . . . . . . . . . . . 13 (Disj 𝑦𝐴 𝑥𝐵 𝐶Disj 𝑧𝐴 𝑥 𝑧 / 𝑦𝐵𝐶)
102101ad3antlr 718 . . . . . . . . . . . 12 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) → Disj 𝑧𝐴 𝑥 𝑧 / 𝑦𝐵𝐶)
103 simplr 756 . . . . . . . . . . . 12 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) → (𝑢𝐴𝑣𝐴))
104 id 22 . . . . . . . . . . . 12 (𝑢𝑣𝑢𝑣)
105 csbeq1 3785 . . . . . . . . . . . . . 14 (𝑧 = 𝑢𝑧 / 𝑦𝐵 = 𝑢 / 𝑦𝐵)
106105iuneq1d 4812 . . . . . . . . . . . . 13 (𝑧 = 𝑢 𝑥 𝑧 / 𝑦𝐵𝐶 = 𝑥 𝑢 / 𝑦𝐵𝐶)
107 csbeq1 3785 . . . . . . . . . . . . . 14 (𝑧 = 𝑣𝑧 / 𝑦𝐵 = 𝑣 / 𝑦𝐵)
108107iuneq1d 4812 . . . . . . . . . . . . 13 (𝑧 = 𝑣 𝑥 𝑧 / 𝑦𝐵𝐶 = 𝑥 𝑣 / 𝑦𝐵𝐶)
109106, 108disji2 4907 . . . . . . . . . . . 12 ((Disj 𝑧𝐴 𝑥 𝑧 / 𝑦𝐵𝐶 ∧ (𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣) → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅)
110102, 103, 104, 109syl2an3an 1402 . . . . . . . . . . 11 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅)
111 sseq0 4233 . . . . . . . . . . 11 (((𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) ⊆ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) ∧ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)
11294, 110, 111syl2an2r 672 . . . . . . . . . 10 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)
11379, 112pm2.61dane 3049 . . . . . . . . 9 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)
114113expr 449 . . . . . . . 8 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) → (¬ 𝑟 = 𝑠 → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
115114orrd 849 . . . . . . 7 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
116115ex 405 . . . . . 6 (((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) → ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)))
117116rexlimdvva 3233 . . . . 5 ((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) → (∃𝑢𝐴𝑣𝐴 (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)))
11859, 117syl5bi 234 . . . 4 ((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) → ((𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)))
119118ralrimivv 3134 . . 3 ((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) → ∀𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
120 disjors 4906 . . 3 (Disj 𝑥 𝑦𝐴 𝐵𝐶 ↔ ∀𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
121119, 120sylibr 226 . 2 ((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) → Disj 𝑥 𝑦𝐴 𝐵𝐶)
12246, 121impbid1 217 1 (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶 ↔ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  wo 833   = wceq 1507  wcel 2048  wne 2961  wral 3082  wrex 3083  csb 3782  cin 3824  wss 3825  c0 4173   ciun 4786  Disj wdisj 4891
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-in 3832  df-ss 3839  df-nul 4174  df-iun 4788  df-disj 4892
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator