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

Theorem disjxiun 5071
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 4959 . . . . . 6 𝑦 𝑦𝐴 𝐵
2 nfcv 2907 . . . . . 6 𝑦𝐶
31, 2nfdisjw 5051 . . . . 5 𝑦Disj 𝑥 𝑦𝐴 𝐵𝐶
4 disjss1 5045 . . . . . 6 (𝐵 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶Disj 𝑥𝐵 𝐶))
5 ssiun2 4977 . . . . . 6 (𝑦𝐴𝐵 𝑦𝐴 𝐵)
64, 5syl11 33 . . . . 5 (Disj 𝑥 𝑦𝐴 𝐵𝐶 → (𝑦𝐴Disj 𝑥𝐵 𝐶))
73, 6ralrimi 3140 . . . 4 (Disj 𝑥 𝑦𝐴 𝐵𝐶 → ∀𝑦𝐴 Disj 𝑥𝐵 𝐶)
87a1i 11 . . 3 (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶 → ∀𝑦𝐴 Disj 𝑥𝐵 𝐶))
9 simplr 766 . . . . . . . . . 10 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → Disj 𝑥 𝑦𝐴 𝐵𝐶)
10 ssiun2 4977 . . . . . . . . . . . . 13 (𝑢𝐴𝑢 / 𝑦𝐵 𝑢𝐴 𝑢 / 𝑦𝐵)
11 nfcv 2907 . . . . . . . . . . . . . 14 𝑢𝐵
12 nfcsb1v 3857 . . . . . . . . . . . . . 14 𝑦𝑢 / 𝑦𝐵
13 csbeq1a 3846 . . . . . . . . . . . . . 14 (𝑦 = 𝑢𝐵 = 𝑢 / 𝑦𝐵)
1411, 12, 13cbviun 4966 . . . . . . . . . . . . 13 𝑦𝐴 𝐵 = 𝑢𝐴 𝑢 / 𝑦𝐵
1510, 14sseqtrrdi 3972 . . . . . . . . . . . 12 (𝑢𝐴𝑢 / 𝑦𝐵 𝑦𝐴 𝐵)
1615adantr 481 . . . . . . . . . . 11 ((𝑢𝐴𝑣𝐴) → 𝑢 / 𝑦𝐵 𝑦𝐴 𝐵)
1716ad2antrl 725 . . . . . . . . . 10 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 / 𝑦𝐵 𝑦𝐴 𝐵)
18 csbeq1 3835 . . . . . . . . . . . . . 14 (𝑢 = 𝑣𝑢 / 𝑦𝐵 = 𝑣 / 𝑦𝐵)
1918sseq1d 3952 . . . . . . . . . . . . 13 (𝑢 = 𝑣 → (𝑢 / 𝑦𝐵 𝑦𝐴 𝐵𝑣 / 𝑦𝐵 𝑦𝐴 𝐵))
2019, 15vtoclga 3511 . . . . . . . . . . . 12 (𝑣𝐴𝑣 / 𝑦𝐵 𝑦𝐴 𝐵)
2120adantl 482 . . . . . . . . . . 11 ((𝑢𝐴𝑣𝐴) → 𝑣 / 𝑦𝐵 𝑦𝐴 𝐵)
2221ad2antrl 725 . . . . . . . . . 10 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 / 𝑦𝐵 𝑦𝐴 𝐵)
2311, 12, 13cbvdisj 5049 . . . . . . . . . . . . . . . 16 (Disj 𝑦𝐴 𝐵Disj 𝑢𝐴 𝑢 / 𝑦𝐵)
2418disjor 5054 . . . . . . . . . . . . . . . 16 (Disj 𝑢𝐴 𝑢 / 𝑦𝐵 ↔ ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅))
2523, 24sylbb 218 . . . . . . . . . . . . . . 15 (Disj 𝑦𝐴 𝐵 → ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅))
26 rsp2 3137 . . . . . . . . . . . . . . 15 (∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅) → ((𝑢𝐴𝑣𝐴) → (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)))
2725, 26syl 17 . . . . . . . . . . . . . 14 (Disj 𝑦𝐴 𝐵 → ((𝑢𝐴𝑣𝐴) → (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)))
2827imp 407 . . . . . . . . . . . . 13 ((Disj 𝑦𝐴 𝐵 ∧ (𝑢𝐴𝑣𝐴)) → (𝑢 = 𝑣 ∨ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅))
2928ord 861 . . . . . . . . . . . 12 ((Disj 𝑦𝐴 𝐵 ∧ (𝑢𝐴𝑣𝐴)) → (¬ 𝑢 = 𝑣 → (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅))
3029impr 455 . . . . . . . . . . 11 ((Disj 𝑦𝐴 𝐵 ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)
3130adantlr 712 . . . . . . . . . 10 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)
32 disjiun 5061 . . . . . . . . . 10 ((Disj 𝑥 𝑦𝐴 𝐵𝐶 ∧ (𝑢 / 𝑦𝐵 𝑦𝐴 𝐵𝑣 / 𝑦𝐵 𝑦𝐴 𝐵 ∧ (𝑢 / 𝑦𝐵𝑣 / 𝑦𝐵) = ∅)) → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅)
339, 17, 22, 31, 32syl13anc 1371 . . . . . . . . 9 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ ((𝑢𝐴𝑣𝐴) ∧ ¬ 𝑢 = 𝑣)) → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅)
3433expr 457 . . . . . . . 8 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ (𝑢𝐴𝑣𝐴)) → (¬ 𝑢 = 𝑣 → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅))
3534orrd 860 . . . . . . 7 (((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) ∧ (𝑢𝐴𝑣𝐴)) → (𝑢 = 𝑣 ∨ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅))
3635ralrimivva 3120 . . . . . 6 ((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) → ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅))
3718iuneq1d 4952 . . . . . . 7 (𝑢 = 𝑣 𝑥 𝑢 / 𝑦𝐵𝐶 = 𝑥 𝑣 / 𝑦𝐵𝐶)
3837disjor 5054 . . . . . 6 (Disj 𝑢𝐴 𝑥 𝑢 / 𝑦𝐵𝐶 ↔ ∀𝑢𝐴𝑣𝐴 (𝑢 = 𝑣 ∨ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅))
3936, 38sylibr 233 . . . . 5 ((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) → Disj 𝑢𝐴 𝑥 𝑢 / 𝑦𝐵𝐶)
40 nfcv 2907 . . . . . 6 𝑢 𝑥𝐵 𝐶
4112, 2nfiun 4955 . . . . . 6 𝑦 𝑥 𝑢 / 𝑦𝐵𝐶
4213iuneq1d 4952 . . . . . 6 (𝑦 = 𝑢 𝑥𝐵 𝐶 = 𝑥 𝑢 / 𝑦𝐵𝐶)
4340, 41, 42cbvdisj 5049 . . . . 5 (Disj 𝑦𝐴 𝑥𝐵 𝐶Disj 𝑢𝐴 𝑥 𝑢 / 𝑦𝐵𝐶)
4439, 43sylibr 233 . . . 4 ((Disj 𝑦𝐴 𝐵Disj 𝑥 𝑦𝐴 𝐵𝐶) → Disj 𝑦𝐴 𝑥𝐵 𝐶)
4544ex 413 . . 3 (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶))
468, 45jcad 513 . 2 (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶 → (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)))
4714eleq2i 2830 . . . . . . . 8 (𝑟 𝑦𝐴 𝐵𝑟 𝑢𝐴 𝑢 / 𝑦𝐵)
48 eliun 4929 . . . . . . . 8 (𝑟 𝑢𝐴 𝑢 / 𝑦𝐵 ↔ ∃𝑢𝐴 𝑟𝑢 / 𝑦𝐵)
4947, 48bitri 274 . . . . . . 7 (𝑟 𝑦𝐴 𝐵 ↔ ∃𝑢𝐴 𝑟𝑢 / 𝑦𝐵)
50 nfcv 2907 . . . . . . . . . 10 𝑣𝐵
51 nfcsb1v 3857 . . . . . . . . . 10 𝑦𝑣 / 𝑦𝐵
52 csbeq1a 3846 . . . . . . . . . 10 (𝑦 = 𝑣𝐵 = 𝑣 / 𝑦𝐵)
5350, 51, 52cbviun 4966 . . . . . . . . 9 𝑦𝐴 𝐵 = 𝑣𝐴 𝑣 / 𝑦𝐵
5453eleq2i 2830 . . . . . . . 8 (𝑠 𝑦𝐴 𝐵𝑠 𝑣𝐴 𝑣 / 𝑦𝐵)
55 eliun 4929 . . . . . . . 8 (𝑠 𝑣𝐴 𝑣 / 𝑦𝐵 ↔ ∃𝑣𝐴 𝑠𝑣 / 𝑦𝐵)
5654, 55bitri 274 . . . . . . 7 (𝑠 𝑦𝐴 𝐵 ↔ ∃𝑣𝐴 𝑠𝑣 / 𝑦𝐵)
5749, 56anbi12i 627 . . . . . 6 ((𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵) ↔ (∃𝑢𝐴 𝑟𝑢 / 𝑦𝐵 ∧ ∃𝑣𝐴 𝑠𝑣 / 𝑦𝐵))
58 reeanv 3292 . . . . . 6 (∃𝑢𝐴𝑣𝐴 (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ↔ (∃𝑢𝐴 𝑟𝑢 / 𝑦𝐵 ∧ ∃𝑣𝐴 𝑠𝑣 / 𝑦𝐵))
5957, 58bitr4i 277 . . . . 5 ((𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵) ↔ ∃𝑢𝐴𝑣𝐴 (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵))
60 simplrr 775 . . . . . . . . . . 11 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → ¬ 𝑟 = 𝑠)
6112, 2nfdisjw 5051 . . . . . . . . . . . . . . . . . . 19 𝑦Disj 𝑥 𝑢 / 𝑦𝐵𝐶
6213disjeq1d 5047 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑢 → (Disj 𝑥𝐵 𝐶Disj 𝑥 𝑢 / 𝑦𝐵𝐶))
6361, 62rspc 3547 . . . . . . . . . . . . . . . . . 18 (𝑢𝐴 → (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑥 𝑢 / 𝑦𝐵𝐶))
6463impcom 408 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝐴 Disj 𝑥𝐵 𝐶𝑢𝐴) → Disj 𝑥 𝑢 / 𝑦𝐵𝐶)
65 disjors 5055 . . . . . . . . . . . . . . . . 17 (Disj 𝑥 𝑢 / 𝑦𝐵𝐶 ↔ ∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
6664, 65sylib 217 . . . . . . . . . . . . . . . 16 ((∀𝑦𝐴 Disj 𝑥𝐵 𝐶𝑢𝐴) → ∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
6766ad2ant2r 744 . . . . . . . . . . . . . . 15 (((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) → ∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
6867adantr 481 . . . . . . . . . . . . . 14 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) → ∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
69 simplrl 774 . . . . . . . . . . . . . . 15 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) ∧ 𝑢 = 𝑣) → 𝑟𝑢 / 𝑦𝐵)
70 simplrr 775 . . . . . . . . . . . . . . . 16 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) ∧ 𝑢 = 𝑣) → 𝑠𝑣 / 𝑦𝐵)
7118adantl 482 . . . . . . . . . . . . . . . 16 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) ∧ 𝑢 = 𝑣) → 𝑢 / 𝑦𝐵 = 𝑣 / 𝑦𝐵)
7270, 71eleqtrrd 2842 . . . . . . . . . . . . . . 15 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) ∧ 𝑢 = 𝑣) → 𝑠𝑢 / 𝑦𝐵)
7369, 72jca 512 . . . . . . . . . . . . . 14 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) ∧ 𝑢 = 𝑣) → (𝑟𝑢 / 𝑦𝐵𝑠𝑢 / 𝑦𝐵))
74 rsp2 3137 . . . . . . . . . . . . . . 15 (∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅) → ((𝑟𝑢 / 𝑦𝐵𝑠𝑢 / 𝑦𝐵) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)))
7574imp 407 . . . . . . . . . . . . . 14 ((∀𝑟 𝑢 / 𝑦𝐵𝑠 𝑢 / 𝑦𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑢 / 𝑦𝐵)) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
7668, 73, 75syl2an2r 682 . . . . . . . . . . . . 13 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
7776adantlrr 718 . . . . . . . . . . . 12 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
7877ord 861 . . . . . . . . . . 11 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (¬ 𝑟 = 𝑠 → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
7960, 78mpd 15 . . . . . . . . . 10 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢 = 𝑣) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)
80 ssiun2 4977 . . . . . . . . . . . . . 14 (𝑟𝑢 / 𝑦𝐵𝑟 / 𝑥𝐶 𝑟 𝑢 / 𝑦𝐵𝑟 / 𝑥𝐶)
81 nfcv 2907 . . . . . . . . . . . . . . 15 𝑟𝐶
82 nfcsb1v 3857 . . . . . . . . . . . . . . 15 𝑥𝑟 / 𝑥𝐶
83 csbeq1a 3846 . . . . . . . . . . . . . . 15 (𝑥 = 𝑟𝐶 = 𝑟 / 𝑥𝐶)
8481, 82, 83cbviun 4966 . . . . . . . . . . . . . 14 𝑥 𝑢 / 𝑦𝐵𝐶 = 𝑟 𝑢 / 𝑦𝐵𝑟 / 𝑥𝐶
8580, 84sseqtrrdi 3972 . . . . . . . . . . . . 13 (𝑟𝑢 / 𝑦𝐵𝑟 / 𝑥𝐶 𝑥 𝑢 / 𝑦𝐵𝐶)
86 ssiun2 4977 . . . . . . . . . . . . . 14 (𝑠𝑣 / 𝑦𝐵𝑠 / 𝑥𝐶 𝑠 𝑣 / 𝑦𝐵𝑠 / 𝑥𝐶)
87 nfcv 2907 . . . . . . . . . . . . . . 15 𝑠𝐶
88 nfcsb1v 3857 . . . . . . . . . . . . . . 15 𝑥𝑠 / 𝑥𝐶
89 csbeq1a 3846 . . . . . . . . . . . . . . 15 (𝑥 = 𝑠𝐶 = 𝑠 / 𝑥𝐶)
9087, 88, 89cbviun 4966 . . . . . . . . . . . . . 14 𝑥 𝑣 / 𝑦𝐵𝐶 = 𝑠 𝑣 / 𝑦𝐵𝑠 / 𝑥𝐶
9186, 90sseqtrrdi 3972 . . . . . . . . . . . . 13 (𝑠𝑣 / 𝑦𝐵𝑠 / 𝑥𝐶 𝑥 𝑣 / 𝑦𝐵𝐶)
92 ss2in 4171 . . . . . . . . . . . . 13 ((𝑟 / 𝑥𝐶 𝑥 𝑢 / 𝑦𝐵𝐶𝑠 / 𝑥𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) ⊆ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶))
9385, 91, 92syl2an 596 . . . . . . . . . . . 12 ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) ⊆ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶))
9493ad2antrl 725 . . . . . . . . . . 11 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) ⊆ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶))
95 nfcv 2907 . . . . . . . . . . . . . . 15 𝑧 𝑥𝐵 𝐶
96 nfcsb1v 3857 . . . . . . . . . . . . . . . 16 𝑦𝑧 / 𝑦𝐵
9796, 2nfiun 4955 . . . . . . . . . . . . . . 15 𝑦 𝑥 𝑧 / 𝑦𝐵𝐶
98 csbeq1a 3846 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧𝐵 = 𝑧 / 𝑦𝐵)
9998iuneq1d 4952 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 𝑥𝐵 𝐶 = 𝑥 𝑧 / 𝑦𝐵𝐶)
10095, 97, 99cbvdisj 5049 . . . . . . . . . . . . . 14 (Disj 𝑦𝐴 𝑥𝐵 𝐶Disj 𝑧𝐴 𝑥 𝑧 / 𝑦𝐵𝐶)
101100biimpi 215 . . . . . . . . . . . . 13 (Disj 𝑦𝐴 𝑥𝐵 𝐶Disj 𝑧𝐴 𝑥 𝑧 / 𝑦𝐵𝐶)
102101ad3antlr 728 . . . . . . . . . . . 12 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) → Disj 𝑧𝐴 𝑥 𝑧 / 𝑦𝐵𝐶)
103 simplr 766 . . . . . . . . . . . 12 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) → (𝑢𝐴𝑣𝐴))
104 id 22 . . . . . . . . . . . 12 (𝑢𝑣𝑢𝑣)
105 csbeq1 3835 . . . . . . . . . . . . . 14 (𝑧 = 𝑢𝑧 / 𝑦𝐵 = 𝑢 / 𝑦𝐵)
106105iuneq1d 4952 . . . . . . . . . . . . 13 (𝑧 = 𝑢 𝑥 𝑧 / 𝑦𝐵𝐶 = 𝑥 𝑢 / 𝑦𝐵𝐶)
107 csbeq1 3835 . . . . . . . . . . . . . 14 (𝑧 = 𝑣𝑧 / 𝑦𝐵 = 𝑣 / 𝑦𝐵)
108107iuneq1d 4952 . . . . . . . . . . . . 13 (𝑧 = 𝑣 𝑥 𝑧 / 𝑦𝐵𝐶 = 𝑥 𝑣 / 𝑦𝐵𝐶)
109106, 108disji2 5056 . . . . . . . . . . . 12 ((Disj 𝑧𝐴 𝑥 𝑧 / 𝑦𝐵𝐶 ∧ (𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣) → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅)
110102, 103, 104, 109syl2an3an 1421 . . . . . . . . . . 11 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅)
111 sseq0 4334 . . . . . . . . . . 11 (((𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) ⊆ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) ∧ ( 𝑥 𝑢 / 𝑦𝐵𝐶 𝑥 𝑣 / 𝑦𝐵𝐶) = ∅) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)
11294, 110, 111syl2an2r 682 . . . . . . . . . 10 (((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) ∧ 𝑢𝑣) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)
11379, 112pm2.61dane 3032 . . . . . . . . 9 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) ∧ ¬ 𝑟 = 𝑠)) → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)
114113expr 457 . . . . . . . 8 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) → (¬ 𝑟 = 𝑠 → (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
115114orrd 860 . . . . . . 7 ((((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) ∧ (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵)) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
116115ex 413 . . . . . 6 (((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) ∧ (𝑢𝐴𝑣𝐴)) → ((𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)))
117116rexlimdvva 3221 . . . . 5 ((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) → (∃𝑢𝐴𝑣𝐴 (𝑟𝑢 / 𝑦𝐵𝑠𝑣 / 𝑦𝐵) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)))
11859, 117syl5bi 241 . . . 4 ((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) → ((𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵) → (𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅)))
119118ralrimivv 3119 . . 3 ((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) → ∀𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
120 disjors 5055 . . 3 (Disj 𝑥 𝑦𝐴 𝐵𝐶 ↔ ∀𝑟 𝑦𝐴 𝐵𝑠 𝑦𝐴 𝐵(𝑟 = 𝑠 ∨ (𝑟 / 𝑥𝐶𝑠 / 𝑥𝐶) = ∅))
121119, 120sylibr 233 . 2 ((∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶) → Disj 𝑥 𝑦𝐴 𝐵𝐶)
12246, 121impbid1 224 1 (Disj 𝑦𝐴 𝐵 → (Disj 𝑥 𝑦𝐴 𝐵𝐶 ↔ (∀𝑦𝐴 Disj 𝑥𝐵 𝐶Disj 𝑦𝐴 𝑥𝐵 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844   = wceq 1539  wcel 2106  wne 2943  wral 3064  wrex 3065  csb 3832  cin 3886  wss 3887  c0 4257   ciun 4925  Disj wdisj 5039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3072  df-rab 3073  df-v 3432  df-sbc 3717  df-csb 3833  df-dif 3890  df-in 3894  df-ss 3904  df-nul 4258  df-iun 4927  df-disj 5040
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator