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

Theorem disjxiunOLD 4580
 Description: Obsolete proof of disjxiun 4579 as of 27-May-2021. 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.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
disjxiunOLD (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶 ↔ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵   𝑦,𝐶
Allowed substitution hints:   𝐵(𝑦)   𝐶(𝑥)

Proof of Theorem disjxiunOLD
Dummy variables 𝑠 𝑟 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfiu1 4486 . . . . . 6 𝑦 𝑦𝐴 𝐵
2 nfcv 2751 . . . . . 6 𝑦𝐶
31, 2nfdisj 4565 . . . . 5 𝑦Disj 𝑥 𝑦𝐴 𝐵𝐶
4 ssiun2 4499 . . . . . . 7 (𝑦𝐴𝐵 𝑦𝐴 𝐵)
5 disjss1 4559 . . . . . . 7 (𝐵 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶Disj 𝑥𝐵 𝐶))
64, 5syl 17 . . . . . 6 (𝑦𝐴 → (Disj 𝑥 𝑦𝐴 𝐵𝐶Disj 𝑥𝐵 𝐶))
76com12 32 . . . . 5 (Disj 𝑥 𝑦𝐴 𝐵𝐶 → (𝑦𝐴Disj 𝑥𝐵 𝐶))
83, 7ralrimi 2940 . . . 4 (Disj 𝑥 𝑦𝐴 𝐵𝐶 → ∀𝑦𝐴 Disj 𝑥𝐵 𝐶)
98a1i 11 . . 3 (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶 → ∀𝑦𝐴 Disj 𝑥𝐵 𝐶))
10 simplr 788 . . . . . . . . . 10 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → Disj 𝑥 𝑦𝐴 𝐵𝐶)
11 simprll 798 . . . . . . . . . . 11 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → 𝑢𝐴)
12 ssiun2 4499 . . . . . . . . . . . 12 (𝑢𝐴𝑢 / 𝑦𝐵 𝑢𝐴 𝑢 / 𝑦𝐵)
13 nfcv 2751 . . . . . . . . . . . . 13 𝑢𝐵
14 nfcsb1v 3515 . . . . . . . . . . . . 13 𝑦𝑢 / 𝑦𝐵
15 csbeq1a 3508 . . . . . . . . . . . . 13 (𝑦 = 𝑢𝐵 = 𝑢 / 𝑦𝐵)
1613, 14, 15cbviun 4493 . . . . . . . . . . . 12 𝑦𝐴 𝐵 = 𝑢𝐴 𝑢 / 𝑦𝐵
1712, 16syl6sseqr 3615 . . . . . . . . . . 11 (𝑢𝐴𝑢 / 𝑦𝐵 𝑦𝐴 𝐵)
1811, 17syl 17 . . . . . . . . . 10 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 / 𝑦𝐵 𝑦𝐴 𝐵)
19 simprlr 799 . . . . . . . . . . 11 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → 𝑣𝐴)
20 csbeq1 3502 . . . . . . . . . . . . 13 (𝑢 = 𝑣𝑢 / 𝑦𝐵 = 𝑣 / 𝑦𝐵)
2120sseq1d 3595 . . . . . . . . . . . 12 (𝑢 = 𝑣 → (𝑢 / 𝑦𝐵 𝑦𝐴 𝐵𝑣 / 𝑦𝐵 𝑦𝐴 𝐵))
2221, 17vtoclga 3245 . . . . . . . . . . 11 (𝑣𝐴𝑣 / 𝑦𝐵 𝑦𝐴 𝐵)
2319, 22syl 17 . . . . . . . . . 10 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 / 𝑦𝐵 𝑦𝐴 𝐵)
24 simpl 472 . . . . . . . . . . . . . . . 16 ((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) → Disj 𝑦𝐴 𝐵)
2513, 14, 15cbvdisj 4563 . . . . . . . . . . . . . . . 16 (Disj 𝑦𝐴 𝐵Disj 𝑢𝐴 𝑢 / 𝑦𝐵)
2624, 25sylib 207 . . . . . . . . . . . . . . 15 ((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) → Disj 𝑢𝐴 𝑢 / 𝑦𝐵)
2720disjor 4567 . . . . . . . . . . . . . . 15 (Disj 𝑢𝐴 𝑢 / 𝑦𝐵 ↔ ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅))
2826, 27sylib 207 . . . . . . . . . . . . . 14 ((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) → ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅))
29 rsp2 2920 . . . . . . . . . . . . . 14 (∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅) → ((𝑢𝐴𝑣𝐴) → (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)))
3028, 29syl 17 . . . . . . . . . . . . 13 ((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) → ((𝑢𝐴𝑣𝐴) → (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)))
3130imp 444 . . . . . . . . . . . 12 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ (𝑢𝐴𝑣𝐴)) → (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅))
3231ord 391 . . . . . . . . . . 11 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ (𝑢𝐴𝑣𝐴)) → (¬ 𝑢 = 𝑣 → (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅))
3332impr 647 . . . . . . . . . 10 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)
34 disjiun 4573 . . . . . . . . . 10 ((Disj 𝑥 𝑦𝐴 𝐵𝐶 ∧ (𝑢 / 𝑦𝐵 𝑦𝐴 𝐵𝑣 / 𝑦𝐵 𝑦𝐴 𝐵 ∧ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)) → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅)
3510, 18, 23, 33, 34syl13anc 1320 . . . . . . . . 9 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅)
3635expr 641 . . . . . . . 8 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ (𝑢𝐴𝑣𝐴)) → (¬ 𝑢 = 𝑣 → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅))
3736orrd 392 . . . . . . 7 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ (𝑢𝐴𝑣𝐴)) → (𝑢 = 𝑣 ∨ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅))
3837ralrimivva 2954 . . . . . 6 ((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) → ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅))
3920iuneq1d 4481 . . . . . . 7 (𝑢 = 𝑣 𝑥 𝑢 / 𝑦𝐵𝐶 = 𝑥 𝑣 / 𝑦𝐵𝐶)
4039disjor 4567 . . . . . 6 (Disj 𝑢𝐴 𝑥 𝑢 / 𝑦𝐵𝐶 ↔ ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅))
4138, 40sylibr 223 . . . . 5 ((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) → Disj 𝑢𝐴 𝑥 𝑢 / 𝑦𝐵𝐶)
42 nfcv 2751 . . . . . 6 𝑢 𝑥𝐵 𝐶
4314, 2nfiun 4484 . . . . . 6 𝑦 𝑥 𝑢 / 𝑦𝐵𝐶
4415iuneq1d 4481 . . . . . 6 (𝑦 = 𝑢 𝑥𝐵 𝐶 = 𝑥 𝑢 / 𝑦𝐵𝐶)
4542, 43, 44cbvdisj 4563 . . . . 5 (Disj 𝑦𝐴 𝑥𝐵 𝐶Disj 𝑢𝐴 𝑥 𝑢 / 𝑦𝐵𝐶)
4641, 45sylibr 223 . . . 4 ((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) → Disj 𝑦𝐴 𝑥𝐵 𝐶)
4746ex 449 . . 3 (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶))
489, 47jcad 554 . 2 (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶 → (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)))
4916eleq2i 2680 . . . . . . . . 9 (𝑟 𝑦𝐴 𝐵𝑟 𝑢𝐴 𝑢 / 𝑦𝐵)
50 eliun 4460 . . . . . . . . 9 (𝑟 𝑢𝐴 𝑢 / 𝑦𝐵 ↔ ∃𝑢𝐴 𝑟𝑢 / 𝑦𝐵)
5149, 50bitri 263 . . . . . . . 8 (𝑟 𝑦𝐴 𝐵 ↔ ∃𝑢𝐴 𝑟𝑢 / 𝑦𝐵)
52 nfcv 2751 . . . . . . . . . . 11 𝑣𝐵
53 nfcsb1v 3515 . . . . . . . . . . 11 𝑦𝑣 / 𝑦𝐵
54 csbeq1a 3508 . . . . . . . . . . 11 (𝑦 = 𝑣𝐵 = 𝑣 / 𝑦𝐵)
5552, 53, 54cbviun 4493 . . . . . . . . . 10 𝑦𝐴 𝐵 = 𝑣𝐴 𝑣 / 𝑦𝐵
5655eleq2i 2680 . . . . . . . . 9 (𝑠 𝑦𝐴 𝐵𝑠 𝑣𝐴 𝑣 / 𝑦𝐵)
57 eliun 4460 . . . . . . . . 9 (𝑠 𝑣𝐴 𝑣 / 𝑦𝐵 ↔ ∃𝑣𝐴 𝑠𝑣 / 𝑦𝐵)
5856, 57bitri 263 . . . . . . . 8 (𝑠 𝑦𝐴 𝐵 ↔ ∃𝑣𝐴 𝑠𝑣 / 𝑦𝐵)
5951, 58anbi12i 729 . . . . . . 7 ((𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵) ↔ (∃𝑢𝐴 𝑟𝑢 / 𝑦𝐵 ∧ ∃𝑣𝐴 𝑠𝑣 / 𝑦𝐵))
60 reeanv 3086 . . . . . . 7 (∃𝑢𝐴𝑣𝐴 (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ↔ (∃𝑢𝐴 𝑟𝑢 / 𝑦𝐵 ∧ ∃𝑣𝐴 𝑠𝑣 / 𝑦𝐵))
6159, 60bitr4i 266 . . . . . 6 ((𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵) ↔ ∃𝑢𝐴𝑣𝐴 (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵))
62 simplrr 797 . . . . . . . . . . . 12 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → ¬ 𝑟 = 𝑠)
63 simprl 790 . . . . . . . . . . . . . . . . 17 (((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) → 𝑢𝐴)
64 simplrl 796 . . . . . . . . . . . . . . . . 17 (((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) → ∀𝑦𝐴 Disj 𝑥𝐵 𝐶)
6514, 2nfdisj 4565 . . . . . . . . . . . . . . . . . 18 𝑦Disj 𝑥 𝑢 / 𝑦𝐵𝐶
6615disjeq1d 4561 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑢 → (Disj 𝑥𝐵 𝐶Disj 𝑥 𝑢 / 𝑦𝐵𝐶))
6765, 66rspc 3276 . . . . . . . . . . . . . . . . 17 (𝑢𝐴 → (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑥 𝑢 / 𝑦𝐵𝐶))
6863, 64, 67sylc 63 . . . . . . . . . . . . . . . 16 (((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) → Disj 𝑥 𝑢 / 𝑦𝐵𝐶)
6968ad2antrr 758 . . . . . . . . . . . . . . 15 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → Disj 𝑥 𝑢 / 𝑦𝐵𝐶)
70 disjors 4568 . . . . . . . . . . . . . . 15 (Disj 𝑥 𝑢 / 𝑦𝐵𝐶 ↔ ∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
7169, 70sylib 207 . . . . . . . . . . . . . 14 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → ∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
72 simplrl 796 . . . . . . . . . . . . . . . 16 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵))
7372simpld 474 . . . . . . . . . . . . . . 15 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → 𝑟𝑢 / 𝑦𝐵)
7472simprd 478 . . . . . . . . . . . . . . . 16 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → 𝑠𝑣 / 𝑦𝐵)
7520adantl 481 . . . . . . . . . . . . . . . 16 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → 𝑢 / 𝑦𝐵 = 𝑣 / 𝑦𝐵)
7674, 75eleqtrrd 2691 . . . . . . . . . . . . . . 15 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → 𝑠𝑢 / 𝑦𝐵)
7773, 76jca 553 . . . . . . . . . . . . . 14 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟𝑢 / 𝑦𝐵𝑠𝑢 / 𝑦𝐵))
78 rsp2 2920 . . . . . . . . . . . . . 14 (∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅) → ((𝑟𝑢 / 𝑦𝐵𝑠𝑢 / 𝑦𝐵) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)))
7971, 77, 78sylc 63 . . . . . . . . . . . . 13 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
8079ord 391 . . . . . . . . . . . 12 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (¬ 𝑟 = 𝑠 → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
8162, 80mpd 15 . . . . . . . . . . 11 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)
82 simplrl 796 . . . . . . . . . . . . . . 15 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵))
8382simpld 474 . . . . . . . . . . . . . 14 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → 𝑟𝑢 / 𝑦𝐵)
84 ssiun2 4499 . . . . . . . . . . . . . . 15 (𝑟𝑢 / 𝑦𝐵𝑟 / 𝑥𝐶 𝑟 𝑢 / 𝑦𝐵𝑟 / 𝑥𝐶)
85 nfcv 2751 . . . . . . . . . . . . . . . 16 𝑟𝐶
86 nfcsb1v 3515 . . . . . . . . . . . . . . . 16 𝑥𝑟 / 𝑥𝐶
87 csbeq1a 3508 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑟𝐶 = 𝑟 / 𝑥𝐶)
8885, 86, 87cbviun 4493 . . . . . . . . . . . . . . 15 𝑥 𝑢 / 𝑦𝐵𝐶 = 𝑟 𝑢 / 𝑦𝐵𝑟 / 𝑥𝐶
8984, 88syl6sseqr 3615 . . . . . . . . . . . . . 14 (𝑟𝑢 / 𝑦𝐵𝑟 / 𝑥𝐶 𝑥 𝑢 / 𝑦𝐵𝐶)
9083, 89syl 17 . . . . . . . . . . . . 13 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → 𝑟 / 𝑥𝐶 𝑥 𝑢 / 𝑦𝐵𝐶)
9182simprd 478 . . . . . . . . . . . . . 14 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → 𝑠𝑣 / 𝑦𝐵)
92 ssiun2 4499 . . . . . . . . . . . . . . 15 (𝑠𝑣 / 𝑦𝐵𝑠 / 𝑥𝐶 𝑠 𝑣 / 𝑦𝐵𝑠 / 𝑥𝐶)
93 nfcv 2751 . . . . . . . . . . . . . . . 16 𝑠𝐶
94 nfcsb1v 3515 . . . . . . . . . . . . . . . 16 𝑥𝑠 / 𝑥𝐶
95 csbeq1a 3508 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑠𝐶 = 𝑠 / 𝑥𝐶)
9693, 94, 95cbviun 4493 . . . . . . . . . . . . . . 15 𝑥 𝑣 / 𝑦𝐵𝐶 = 𝑠 𝑣 / 𝑦𝐵𝑠 / 𝑥𝐶
9792, 96syl6sseqr 3615 . . . . . . . . . . . . . 14 (𝑠𝑣 / 𝑦𝐵𝑠 / 𝑥𝐶 𝑥 𝑣 / 𝑦𝐵𝐶)
9891, 97syl 17 . . . . . . . . . . . . 13 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → 𝑠 / 𝑥𝐶 𝑥 𝑣 / 𝑦𝐵𝐶)
99 ss2in 3802 . . . . . . . . . . . . 13 ((𝑟 / 𝑥𝐶 𝑥 𝑢 / 𝑦𝐵𝐶𝑠 / 𝑥𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) ⊆ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶))
10090, 98, 99syl2anc 691 . . . . . . . . . . . 12 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) ⊆ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶))
101 simplrr 797 . . . . . . . . . . . . . . 15 (((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) → Disj 𝑦𝐴 𝑥𝐵 𝐶)
102101ad2antrr 758 . . . . . . . . . . . . . 14 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → Disj 𝑦𝐴 𝑥𝐵 𝐶)
103 nfcv 2751 . . . . . . . . . . . . . . 15 𝑧 𝑥𝐵 𝐶
104 nfcsb1v 3515 . . . . . . . . . . . . . . . 16 𝑦𝑧 / 𝑦𝐵
105104, 2nfiun 4484 . . . . . . . . . . . . . . 15 𝑦 𝑥 𝑧 / 𝑦𝐵𝐶
106 csbeq1a 3508 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧𝐵 = 𝑧 / 𝑦𝐵)
107106iuneq1d 4481 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 𝑥𝐵 𝐶 = 𝑥 𝑧 / 𝑦𝐵𝐶)
108103, 105, 107cbvdisj 4563 . . . . . . . . . . . . . 14 (Disj 𝑦𝐴 𝑥𝐵 𝐶Disj 𝑧𝐴 𝑥 𝑧 / 𝑦𝐵𝐶)
109102, 108sylib 207 . . . . . . . . . . . . 13 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → Disj 𝑧𝐴 𝑥 𝑧 / 𝑦𝐵𝐶)
11063ad2antrr 758 . . . . . . . . . . . . 13 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → 𝑢𝐴)
111 simprr 792 . . . . . . . . . . . . . 14 (((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) → 𝑣𝐴)
112111ad2antrr 758 . . . . . . . . . . . . 13 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → 𝑣𝐴)
113 simpr 476 . . . . . . . . . . . . 13 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → 𝑢𝑣)
114 csbeq1 3502 . . . . . . . . . . . . . . 15 (𝑧 = 𝑢𝑧 / 𝑦𝐵 = 𝑢 / 𝑦𝐵)
115114iuneq1d 4481 . . . . . . . . . . . . . 14 (𝑧 = 𝑢 𝑥 𝑧 / 𝑦𝐵𝐶 = 𝑥 𝑢 / 𝑦𝐵𝐶)
116 csbeq1 3502 . . . . . . . . . . . . . . 15 (𝑧 = 𝑣𝑧 / 𝑦𝐵 = 𝑣 / 𝑦𝐵)
117116iuneq1d 4481 . . . . . . . . . . . . . 14 (𝑧 = 𝑣 𝑥 𝑧 / 𝑦𝐵𝐶 = 𝑥 𝑣 / 𝑦𝐵𝐶)
118115, 117disji2 4569 . . . . . . . . . . . . 13 ((Disj 𝑧𝐴 𝑥 𝑧 / 𝑦𝐵𝐶 ∧ (𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣) → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅)
119109, 110, 112, 113, 118syl121anc 1323 . . . . . . . . . . . 12 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅)
120 sseq0 3927 . . . . . . . . . . . 12 (((𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) ⊆ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) ∧ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)
121100, 119, 120syl2anc 691 . . . . . . . . . . 11 (((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)
12281, 121pm2.61dane 2869 . . . . . . . . . 10 ((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)
123122expr 641 . . . . . . . . 9 ((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) → (¬ 𝑟 = 𝑠 → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
124123orrd 392 . . . . . . . 8 ((((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
125124ex 449 . . . . . . 7 (((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) ∧ (𝑢𝐴𝑣𝐴)) → ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)))
126125rexlimdvva 3020 . . . . . 6 ((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) → (∃𝑢𝐴𝑣𝐴 (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)))
12761, 126syl5bi 231 . . . . 5 ((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) → ((𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)))
128127ralrimivv 2953 . . . 4 ((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) → ∀𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
129 disjors 4568 . . . 4 (Disj 𝑥 𝑦𝐴 𝐵𝐶 ↔ ∀𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
130128, 129sylibr 223 . . 3 ((Disj 𝑦𝐴 𝐵 ∧ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)) → Disj 𝑥 𝑦𝐴 𝐵𝐶)
131130ex 449 . 2 (Disj 𝑦𝐴 𝐵 → ((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) → Disj 𝑥 𝑦𝐴 𝐵𝐶))
13248, 131impbid 201 1 (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶 ↔ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  ⦋csb 3499   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ∪ ciun 4455  Disj wdisj 4553 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875  df-iun 4457  df-disj 4554 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator