Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  disjunsn Structured version   Visualization version   GIF version

Theorem disjunsn 30330
Description: Append an element to a disjoint collection. Similar to ralunsn 4797, gsumunsn 19058, etc. (Contributed by Thierry Arnoux, 28-Mar-2018.)
Hypothesis
Ref Expression
disjunsn.s (𝑥 = 𝑀𝐵 = 𝐶)
Assertion
Ref Expression
disjunsn ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝑀   𝑥,𝑉
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem disjunsn
Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 disjors 5020 . . . . . 6 (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
2 eqeq1 2825 . . . . . . . . 9 (𝑖 = 𝑀 → (𝑖 = 𝑗𝑀 = 𝑗))
3 csbeq1 3860 . . . . . . . . . . 11 (𝑖 = 𝑀𝑖 / 𝑥𝐵 = 𝑀 / 𝑥𝐵)
43ineq1d 4163 . . . . . . . . . 10 (𝑖 = 𝑀 → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵))
54eqeq1d 2823 . . . . . . . . 9 (𝑖 = 𝑀 → ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
62, 5orbi12d 916 . . . . . . . 8 (𝑖 = 𝑀 → ((𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
76ralbidv 3185 . . . . . . 7 (𝑖 = 𝑀 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
87ralunsn 4797 . . . . . 6 (𝑀𝑉 → (∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
91, 8syl5bb 286 . . . . 5 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
10 eqeq2 2833 . . . . . . . . 9 (𝑗 = 𝑀 → (𝑖 = 𝑗𝑖 = 𝑀))
11 csbeq1 3860 . . . . . . . . . . 11 (𝑗 = 𝑀𝑗 / 𝑥𝐵 = 𝑀 / 𝑥𝐵)
1211ineq2d 4164 . . . . . . . . . 10 (𝑗 = 𝑀 → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵))
1312eqeq1d 2823 . . . . . . . . 9 (𝑗 = 𝑀 → ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
1410, 13orbi12d 916 . . . . . . . 8 (𝑗 = 𝑀 → ((𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
1514ralunsn 4797 . . . . . . 7 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
1615ralbidv 3185 . . . . . 6 (𝑀𝑉 → (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
17 eqeq2 2833 . . . . . . . . 9 (𝑗 = 𝑀 → (𝑀 = 𝑗𝑀 = 𝑀))
1811ineq2d 4164 . . . . . . . . . 10 (𝑗 = 𝑀 → (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵))
1918eqeq1d 2823 . . . . . . . . 9 (𝑗 = 𝑀 → ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
2017, 19orbi12d 916 . . . . . . . 8 (𝑗 = 𝑀 → ((𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
2120ralunsn 4797 . . . . . . 7 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
22 eqid 2821 . . . . . . . . 9 𝑀 = 𝑀
2322orci 862 . . . . . . . 8 (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)
2423biantru 533 . . . . . . 7 (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
2521, 24syl6bbr 292 . . . . . 6 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
2616, 25anbi12d 633 . . . . 5 (𝑀𝑉 → ((∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
279, 26bitrd 282 . . . 4 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
28 r19.26 3158 . . . . . 6 (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
29 disjors 5020 . . . . . . 7 (Disj 𝑥𝐴 𝐵 ↔ ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
3029anbi1i 626 . . . . . 6 ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
3128, 30bitr4i 281 . . . . 5 (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
3231anbi1i 626 . . . 4 ((∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
3327, 32syl6bb 290 . . 3 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
3433adantr 484 . 2 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
35 orcom 867 . . . . . . . . 9 (((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
3635ralbii 3153 . . . . . . . 8 (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
37 r19.30 3323 . . . . . . . . 9 (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀))
38 risset 3253 . . . . . . . . . . . 12 (𝑀𝐴 ↔ ∃𝑖𝐴 𝑖 = 𝑀)
39 biorf 934 . . . . . . . . . . . 12 (¬ ∃𝑖𝐴 𝑖 = 𝑀 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
4038, 39sylnbi 333 . . . . . . . . . . 11 𝑀𝐴 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
4140adantl 485 . . . . . . . . . 10 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
42 orcom 867 . . . . . . . . . 10 ((∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀))
4341, 42syl6bb 290 . . . . . . . . 9 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀)))
4437, 43syl5ibr 249 . . . . . . . 8 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) → ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4536, 44syl5bir 246 . . . . . . 7 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) → ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
46 olc 865 . . . . . . . 8 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ → (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4746ralimi 3148 . . . . . . 7 (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ → ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4845, 47impbid1 228 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
49 nfv 1916 . . . . . . . . . 10 𝑖(𝐵𝐶) = ∅
50 nfcsb1v 3881 . . . . . . . . . . . 12 𝑥𝑖 / 𝑥𝐵
51 nfcv 2974 . . . . . . . . . . . 12 𝑥𝐶
5250, 51nfin 4168 . . . . . . . . . . 11 𝑥(𝑖 / 𝑥𝐵𝐶)
5352nfeq1 2989 . . . . . . . . . 10 𝑥(𝑖 / 𝑥𝐵𝐶) = ∅
54 csbeq1a 3871 . . . . . . . . . . . 12 (𝑥 = 𝑖𝐵 = 𝑖 / 𝑥𝐵)
5554ineq1d 4163 . . . . . . . . . . 11 (𝑥 = 𝑖 → (𝐵𝐶) = (𝑖 / 𝑥𝐵𝐶))
5655eqeq1d 2823 . . . . . . . . . 10 (𝑥 = 𝑖 → ((𝐵𝐶) = ∅ ↔ (𝑖 / 𝑥𝐵𝐶) = ∅))
5749, 53, 56cbvralw 3418 . . . . . . . . 9 (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅)
5857a1i 11 . . . . . . . 8 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅))
59 ss0b 4324 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ 𝑥𝐴 (𝐵𝐶) = ∅)
60 iunss 4942 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) ⊆ ∅)
61 iunin1 4967 . . . . . . . . . . . 12 𝑥𝐴 (𝐵𝐶) = ( 𝑥𝐴 𝐵𝐶)
6261eqeq1i 2826 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) = ∅ ↔ ( 𝑥𝐴 𝐵𝐶) = ∅)
6359, 60, 623bitr3ri 305 . . . . . . . . . 10 (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) ⊆ ∅)
64 ss0b 4324 . . . . . . . . . . 11 ((𝐵𝐶) ⊆ ∅ ↔ (𝐵𝐶) = ∅)
6564ralbii 3153 . . . . . . . . . 10 (∀𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅)
6663, 65bitri 278 . . . . . . . . 9 (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅)
6766a1i 11 . . . . . . . 8 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅))
68 nfcvd 2975 . . . . . . . . . . . 12 (𝑀𝑉𝑥𝐶)
69 disjunsn.s . . . . . . . . . . . 12 (𝑥 = 𝑀𝐵 = 𝐶)
7068, 69csbiegf 3890 . . . . . . . . . . 11 (𝑀𝑉𝑀 / 𝑥𝐵 = 𝐶)
7170ineq2d 4164 . . . . . . . . . 10 (𝑀𝑉 → (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = (𝑖 / 𝑥𝐵𝐶))
7271eqeq1d 2823 . . . . . . . . 9 (𝑀𝑉 → ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (𝑖 / 𝑥𝐵𝐶) = ∅))
7372ralbidv 3185 . . . . . . . 8 (𝑀𝑉 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅))
7458, 67, 733bitr4d 314 . . . . . . 7 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
7574adantr 484 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
7648, 75bitr4d 285 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅))
7776anbi2d 631 . . . 4 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
78 orcom 867 . . . . . . . 8 (((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
7978ralbii 3153 . . . . . . 7 (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
80 r19.30 3323 . . . . . . . 8 (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗))
81 clel5 3634 . . . . . . . . . . 11 (𝑀𝐴 ↔ ∃𝑗𝐴 𝑀 = 𝑗)
82 biorf 934 . . . . . . . . . . 11 (¬ ∃𝑗𝐴 𝑀 = 𝑗 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
8381, 82sylnbi 333 . . . . . . . . . 10 𝑀𝐴 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
8483adantl 485 . . . . . . . . 9 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
85 orcom 867 . . . . . . . . 9 ((∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗))
8684, 85syl6bb 290 . . . . . . . 8 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗)))
8780, 86syl5ibr 249 . . . . . . 7 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) → ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
8879, 87syl5bir 246 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) → ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
89 olc 865 . . . . . . 7 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
9089ralimi 3148 . . . . . 6 (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
9188, 90impbid1 228 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
92 nfv 1916 . . . . . . . . . 10 𝑗(𝐵𝐶) = ∅
93 nfcsb1v 3881 . . . . . . . . . . . 12 𝑥𝑗 / 𝑥𝐵
9493, 51nfin 4168 . . . . . . . . . . 11 𝑥(𝑗 / 𝑥𝐵𝐶)
9594nfeq1 2989 . . . . . . . . . 10 𝑥(𝑗 / 𝑥𝐵𝐶) = ∅
96 csbeq1a 3871 . . . . . . . . . . . 12 (𝑥 = 𝑗𝐵 = 𝑗 / 𝑥𝐵)
9796ineq1d 4163 . . . . . . . . . . 11 (𝑥 = 𝑗 → (𝐵𝐶) = (𝑗 / 𝑥𝐵𝐶))
9897eqeq1d 2823 . . . . . . . . . 10 (𝑥 = 𝑗 → ((𝐵𝐶) = ∅ ↔ (𝑗 / 𝑥𝐵𝐶) = ∅))
9992, 95, 98cbvralw 3418 . . . . . . . . 9 (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅)
10099a1i 11 . . . . . . . 8 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅))
101 incom 4153 . . . . . . . . . 10 (𝑗 / 𝑥𝐵𝐶) = (𝐶𝑗 / 𝑥𝐵)
102101eqeq1i 2826 . . . . . . . . 9 ((𝑗 / 𝑥𝐵𝐶) = ∅ ↔ (𝐶𝑗 / 𝑥𝐵) = ∅)
103102ralbii 3153 . . . . . . . 8 (∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅)
104100, 103syl6bb 290 . . . . . . 7 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅))
10570ineq1d 4163 . . . . . . . . 9 (𝑀𝑉 → (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝐶𝑗 / 𝑥𝐵))
106105eqeq1d 2823 . . . . . . . 8 (𝑀𝑉 → ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝐶𝑗 / 𝑥𝐵) = ∅))
107106ralbidv 3185 . . . . . . 7 (𝑀𝑉 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅))
108104, 67, 1073bitr4d 314 . . . . . 6 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
109108adantr 484 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
11091, 109bitr4d 285 . . . 4 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅))
11177, 110anbi12d 633 . . 3 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ ((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
112 anass 472 . . . 4 (((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐵 ∧ (( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
113 anidm 568 . . . . 5 ((( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅)
114113anbi2i 625 . . . 4 ((Disj 𝑥𝐴 𝐵 ∧ (( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅))
115112, 114bitri 278 . . 3 (((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅))
116111, 115syl6bb 290 . 2 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
11734, 116bitrd 282 1 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844   = wceq 1538  wcel 2115  wral 3126  wrex 3127  csb 3857  cun 3908  cin 3909  wss 3910  c0 4266  {csn 4540   ciun 4892  Disj wdisj 5004
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-sn 4541  df-iun 4894  df-disj 5005
This theorem is referenced by:  disjun0  30331  disjiunel  30332
  Copyright terms: Public domain W3C validator