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 29275
Description: Append an element to a disjoint collection. Similar to ralunsn 4395, gsumunsn 18291, 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 4603 . . . . . 6 (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
2 eqeq1 2625 . . . . . . . . 9 (𝑖 = 𝑀 → (𝑖 = 𝑗𝑀 = 𝑗))
3 csbeq1 3521 . . . . . . . . . . 11 (𝑖 = 𝑀𝑖 / 𝑥𝐵 = 𝑀 / 𝑥𝐵)
43ineq1d 3796 . . . . . . . . . 10 (𝑖 = 𝑀 → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵))
54eqeq1d 2623 . . . . . . . . 9 (𝑖 = 𝑀 → ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
62, 5orbi12d 745 . . . . . . . 8 (𝑖 = 𝑀 → ((𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
76ralbidv 2981 . . . . . . 7 (𝑖 = 𝑀 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
87ralunsn 4395 . . . . . 6 (𝑀𝑉 → (∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
91, 8syl5bb 272 . . . . 5 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
10 eqeq2 2632 . . . . . . . . 9 (𝑗 = 𝑀 → (𝑖 = 𝑗𝑖 = 𝑀))
11 csbeq1 3521 . . . . . . . . . . 11 (𝑗 = 𝑀𝑗 / 𝑥𝐵 = 𝑀 / 𝑥𝐵)
1211ineq2d 3797 . . . . . . . . . 10 (𝑗 = 𝑀 → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵))
1312eqeq1d 2623 . . . . . . . . 9 (𝑗 = 𝑀 → ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
1410, 13orbi12d 745 . . . . . . . 8 (𝑗 = 𝑀 → ((𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
1514ralunsn 4395 . . . . . . 7 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
1615ralbidv 2981 . . . . . 6 (𝑀𝑉 → (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
17 eqeq2 2632 . . . . . . . . 9 (𝑗 = 𝑀 → (𝑀 = 𝑗𝑀 = 𝑀))
1811ineq2d 3797 . . . . . . . . . 10 (𝑗 = 𝑀 → (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵))
1918eqeq1d 2623 . . . . . . . . 9 (𝑗 = 𝑀 → ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
2017, 19orbi12d 745 . . . . . . . 8 (𝑗 = 𝑀 → ((𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
2120ralunsn 4395 . . . . . . 7 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
22 eqid 2621 . . . . . . . . 9 𝑀 = 𝑀
2322orci 405 . . . . . . . 8 (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)
2423biantru 526 . . . . . . 7 (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
2521, 24syl6bbr 278 . . . . . 6 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
2616, 25anbi12d 746 . . . . 5 (𝑀𝑉 → ((∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
279, 26bitrd 268 . . . 4 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
28 r19.26 3058 . . . . . 6 (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
29 disjors 4603 . . . . . . 7 (Disj 𝑥𝐴 𝐵 ↔ ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
3029anbi1i 730 . . . . . 6 ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
3128, 30bitr4i 267 . . . . 5 (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
3231anbi1i 730 . . . 4 ((∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
3327, 32syl6bb 276 . . 3 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
3433adantr 481 . 2 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
35 orcom 402 . . . . . . . . 9 (((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
3635ralbii 2975 . . . . . . . 8 (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
37 r19.30 3075 . . . . . . . . 9 (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀))
38 risset 3056 . . . . . . . . . . . 12 (𝑀𝐴 ↔ ∃𝑖𝐴 𝑖 = 𝑀)
39 biorf 420 . . . . . . . . . . . 12 (¬ ∃𝑖𝐴 𝑖 = 𝑀 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
4038, 39sylnbi 320 . . . . . . . . . . 11 𝑀𝐴 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
4140adantl 482 . . . . . . . . . 10 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
42 orcom 402 . . . . . . . . . 10 ((∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀))
4341, 42syl6bb 276 . . . . . . . . 9 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀)))
4437, 43syl5ibr 236 . . . . . . . 8 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) → ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4536, 44syl5bir 233 . . . . . . 7 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) → ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
46 olc 399 . . . . . . . 8 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ → (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4746ralimi 2947 . . . . . . 7 (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ → ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4845, 47impbid1 215 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
49 nfv 1840 . . . . . . . . . 10 𝑖(𝐵𝐶) = ∅
50 nfcsb1v 3534 . . . . . . . . . . . 12 𝑥𝑖 / 𝑥𝐵
51 nfcv 2761 . . . . . . . . . . . 12 𝑥𝐶
5250, 51nfin 3803 . . . . . . . . . . 11 𝑥(𝑖 / 𝑥𝐵𝐶)
5352nfeq1 2774 . . . . . . . . . 10 𝑥(𝑖 / 𝑥𝐵𝐶) = ∅
54 csbeq1a 3527 . . . . . . . . . . . 12 (𝑥 = 𝑖𝐵 = 𝑖 / 𝑥𝐵)
5554ineq1d 3796 . . . . . . . . . . 11 (𝑥 = 𝑖 → (𝐵𝐶) = (𝑖 / 𝑥𝐵𝐶))
5655eqeq1d 2623 . . . . . . . . . 10 (𝑥 = 𝑖 → ((𝐵𝐶) = ∅ ↔ (𝑖 / 𝑥𝐵𝐶) = ∅))
5749, 53, 56cbvral 3158 . . . . . . . . 9 (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅)
5857a1i 11 . . . . . . . 8 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅))
59 ss0b 3950 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ 𝑥𝐴 (𝐵𝐶) = ∅)
60 iunss 4532 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) ⊆ ∅)
61 iunin1 4556 . . . . . . . . . . . 12 𝑥𝐴 (𝐵𝐶) = ( 𝑥𝐴 𝐵𝐶)
6261eqeq1i 2626 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) = ∅ ↔ ( 𝑥𝐴 𝐵𝐶) = ∅)
6359, 60, 623bitr3ri 291 . . . . . . . . . 10 (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) ⊆ ∅)
64 ss0b 3950 . . . . . . . . . . 11 ((𝐵𝐶) ⊆ ∅ ↔ (𝐵𝐶) = ∅)
6564ralbii 2975 . . . . . . . . . 10 (∀𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅)
6663, 65bitri 264 . . . . . . . . 9 (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅)
6766a1i 11 . . . . . . . 8 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅))
68 nfcvd 2762 . . . . . . . . . . . 12 (𝑀𝑉𝑥𝐶)
69 disjunsn.s . . . . . . . . . . . 12 (𝑥 = 𝑀𝐵 = 𝐶)
7068, 69csbiegf 3542 . . . . . . . . . . 11 (𝑀𝑉𝑀 / 𝑥𝐵 = 𝐶)
7170ineq2d 3797 . . . . . . . . . 10 (𝑀𝑉 → (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = (𝑖 / 𝑥𝐵𝐶))
7271eqeq1d 2623 . . . . . . . . 9 (𝑀𝑉 → ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (𝑖 / 𝑥𝐵𝐶) = ∅))
7372ralbidv 2981 . . . . . . . 8 (𝑀𝑉 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅))
7458, 67, 733bitr4d 300 . . . . . . 7 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
7574adantr 481 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
7648, 75bitr4d 271 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅))
7776anbi2d 739 . . . 4 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
78 orcom 402 . . . . . . . 8 (((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
7978ralbii 2975 . . . . . . 7 (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
80 r19.30 3075 . . . . . . . 8 (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗))
81 clel5 3330 . . . . . . . . . . 11 (𝑀𝐴 ↔ ∃𝑗𝐴 𝑀 = 𝑗)
82 biorf 420 . . . . . . . . . . 11 (¬ ∃𝑗𝐴 𝑀 = 𝑗 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
8381, 82sylnbi 320 . . . . . . . . . 10 𝑀𝐴 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
8483adantl 482 . . . . . . . . 9 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
85 orcom 402 . . . . . . . . 9 ((∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗))
8684, 85syl6bb 276 . . . . . . . 8 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗)))
8780, 86syl5ibr 236 . . . . . . 7 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) → ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
8879, 87syl5bir 233 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) → ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
89 olc 399 . . . . . . 7 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
9089ralimi 2947 . . . . . 6 (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
9188, 90impbid1 215 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
92 nfv 1840 . . . . . . . . . 10 𝑗(𝐵𝐶) = ∅
93 nfcsb1v 3534 . . . . . . . . . . . 12 𝑥𝑗 / 𝑥𝐵
9493, 51nfin 3803 . . . . . . . . . . 11 𝑥(𝑗 / 𝑥𝐵𝐶)
9594nfeq1 2774 . . . . . . . . . 10 𝑥(𝑗 / 𝑥𝐵𝐶) = ∅
96 csbeq1a 3527 . . . . . . . . . . . 12 (𝑥 = 𝑗𝐵 = 𝑗 / 𝑥𝐵)
9796ineq1d 3796 . . . . . . . . . . 11 (𝑥 = 𝑗 → (𝐵𝐶) = (𝑗 / 𝑥𝐵𝐶))
9897eqeq1d 2623 . . . . . . . . . 10 (𝑥 = 𝑗 → ((𝐵𝐶) = ∅ ↔ (𝑗 / 𝑥𝐵𝐶) = ∅))
9992, 95, 98cbvral 3158 . . . . . . . . 9 (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅)
10099a1i 11 . . . . . . . 8 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅))
101 incom 3788 . . . . . . . . . 10 (𝑗 / 𝑥𝐵𝐶) = (𝐶𝑗 / 𝑥𝐵)
102101eqeq1i 2626 . . . . . . . . 9 ((𝑗 / 𝑥𝐵𝐶) = ∅ ↔ (𝐶𝑗 / 𝑥𝐵) = ∅)
103102ralbii 2975 . . . . . . . 8 (∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅)
104100, 103syl6bb 276 . . . . . . 7 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅))
10570ineq1d 3796 . . . . . . . . 9 (𝑀𝑉 → (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝐶𝑗 / 𝑥𝐵))
106105eqeq1d 2623 . . . . . . . 8 (𝑀𝑉 → ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝐶𝑗 / 𝑥𝐵) = ∅))
107106ralbidv 2981 . . . . . . 7 (𝑀𝑉 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅))
108104, 67, 1073bitr4d 300 . . . . . 6 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
109108adantr 481 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
11091, 109bitr4d 271 . . . 4 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅))
11177, 110anbi12d 746 . . 3 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ ((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
112 anass 680 . . . 4 (((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐵 ∧ (( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
113 anidm 675 . . . . 5 ((( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅)
114113anbi2i 729 . . . 4 ((Disj 𝑥𝐴 𝐵 ∧ (( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅))
115112, 114bitri 264 . . 3 (((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅))
116111, 115syl6bb 276 . 2 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
11734, 116bitrd 268 1 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1987  wral 2907  wrex 2908  csb 3518  cun 3557  cin 3558  wss 3559  c0 3896  {csn 4153   ciun 4490  Disj wdisj 4588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-sn 4154  df-iun 4492  df-disj 4589
This theorem is referenced by:  disjun0  29276  disjiunel  29277
  Copyright terms: Public domain W3C validator