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 30272
Description: Append an element to a disjoint collection. Similar to ralunsn 4816, gsumunsn 19009, 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 5038 . . . . . 6 (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
2 eqeq1 2822 . . . . . . . . 9 (𝑖 = 𝑀 → (𝑖 = 𝑗𝑀 = 𝑗))
3 csbeq1 3883 . . . . . . . . . . 11 (𝑖 = 𝑀𝑖 / 𝑥𝐵 = 𝑀 / 𝑥𝐵)
43ineq1d 4185 . . . . . . . . . 10 (𝑖 = 𝑀 → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵))
54eqeq1d 2820 . . . . . . . . 9 (𝑖 = 𝑀 → ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
62, 5orbi12d 912 . . . . . . . 8 (𝑖 = 𝑀 → ((𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
76ralbidv 3194 . . . . . . 7 (𝑖 = 𝑀 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
87ralunsn 4816 . . . . . 6 (𝑀𝑉 → (∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
91, 8syl5bb 284 . . . . 5 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
10 eqeq2 2830 . . . . . . . . 9 (𝑗 = 𝑀 → (𝑖 = 𝑗𝑖 = 𝑀))
11 csbeq1 3883 . . . . . . . . . . 11 (𝑗 = 𝑀𝑗 / 𝑥𝐵 = 𝑀 / 𝑥𝐵)
1211ineq2d 4186 . . . . . . . . . 10 (𝑗 = 𝑀 → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵))
1312eqeq1d 2820 . . . . . . . . 9 (𝑗 = 𝑀 → ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
1410, 13orbi12d 912 . . . . . . . 8 (𝑗 = 𝑀 → ((𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
1514ralunsn 4816 . . . . . . 7 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
1615ralbidv 3194 . . . . . 6 (𝑀𝑉 → (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
17 eqeq2 2830 . . . . . . . . 9 (𝑗 = 𝑀 → (𝑀 = 𝑗𝑀 = 𝑀))
1811ineq2d 4186 . . . . . . . . . 10 (𝑗 = 𝑀 → (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵))
1918eqeq1d 2820 . . . . . . . . 9 (𝑗 = 𝑀 → ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
2017, 19orbi12d 912 . . . . . . . 8 (𝑗 = 𝑀 → ((𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
2120ralunsn 4816 . . . . . . 7 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
22 eqid 2818 . . . . . . . . 9 𝑀 = 𝑀
2322orci 859 . . . . . . . 8 (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)
2423biantru 530 . . . . . . 7 (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
2521, 24syl6bbr 290 . . . . . 6 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
2616, 25anbi12d 630 . . . . 5 (𝑀𝑉 → ((∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
279, 26bitrd 280 . . . 4 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
28 r19.26 3167 . . . . . 6 (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
29 disjors 5038 . . . . . . 7 (Disj 𝑥𝐴 𝐵 ↔ ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
3029anbi1i 623 . . . . . 6 ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
3128, 30bitr4i 279 . . . . 5 (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
3231anbi1i 623 . . . 4 ((∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
3327, 32syl6bb 288 . . 3 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
3433adantr 481 . 2 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
35 orcom 864 . . . . . . . . 9 (((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
3635ralbii 3162 . . . . . . . 8 (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
37 r19.30 3335 . . . . . . . . 9 (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀))
38 risset 3264 . . . . . . . . . . . 12 (𝑀𝐴 ↔ ∃𝑖𝐴 𝑖 = 𝑀)
39 biorf 930 . . . . . . . . . . . 12 (¬ ∃𝑖𝐴 𝑖 = 𝑀 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
4038, 39sylnbi 331 . . . . . . . . . . 11 𝑀𝐴 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
4140adantl 482 . . . . . . . . . 10 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
42 orcom 864 . . . . . . . . . 10 ((∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀))
4341, 42syl6bb 288 . . . . . . . . 9 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀)))
4437, 43syl5ibr 247 . . . . . . . 8 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) → ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4536, 44syl5bir 244 . . . . . . 7 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) → ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
46 olc 862 . . . . . . . 8 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ → (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4746ralimi 3157 . . . . . . 7 (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ → ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4845, 47impbid1 226 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
49 nfv 1906 . . . . . . . . . 10 𝑖(𝐵𝐶) = ∅
50 nfcsb1v 3904 . . . . . . . . . . . 12 𝑥𝑖 / 𝑥𝐵
51 nfcv 2974 . . . . . . . . . . . 12 𝑥𝐶
5250, 51nfin 4190 . . . . . . . . . . 11 𝑥(𝑖 / 𝑥𝐵𝐶)
5352nfeq1 2990 . . . . . . . . . 10 𝑥(𝑖 / 𝑥𝐵𝐶) = ∅
54 csbeq1a 3894 . . . . . . . . . . . 12 (𝑥 = 𝑖𝐵 = 𝑖 / 𝑥𝐵)
5554ineq1d 4185 . . . . . . . . . . 11 (𝑥 = 𝑖 → (𝐵𝐶) = (𝑖 / 𝑥𝐵𝐶))
5655eqeq1d 2820 . . . . . . . . . 10 (𝑥 = 𝑖 → ((𝐵𝐶) = ∅ ↔ (𝑖 / 𝑥𝐵𝐶) = ∅))
5749, 53, 56cbvralw 3439 . . . . . . . . 9 (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅)
5857a1i 11 . . . . . . . 8 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅))
59 ss0b 4348 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ 𝑥𝐴 (𝐵𝐶) = ∅)
60 iunss 4960 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) ⊆ ∅)
61 iunin1 4985 . . . . . . . . . . . 12 𝑥𝐴 (𝐵𝐶) = ( 𝑥𝐴 𝐵𝐶)
6261eqeq1i 2823 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) = ∅ ↔ ( 𝑥𝐴 𝐵𝐶) = ∅)
6359, 60, 623bitr3ri 303 . . . . . . . . . 10 (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) ⊆ ∅)
64 ss0b 4348 . . . . . . . . . . 11 ((𝐵𝐶) ⊆ ∅ ↔ (𝐵𝐶) = ∅)
6564ralbii 3162 . . . . . . . . . 10 (∀𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅)
6663, 65bitri 276 . . . . . . . . 9 (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅)
6766a1i 11 . . . . . . . 8 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅))
68 nfcvd 2975 . . . . . . . . . . . 12 (𝑀𝑉𝑥𝐶)
69 disjunsn.s . . . . . . . . . . . 12 (𝑥 = 𝑀𝐵 = 𝐶)
7068, 69csbiegf 3913 . . . . . . . . . . 11 (𝑀𝑉𝑀 / 𝑥𝐵 = 𝐶)
7170ineq2d 4186 . . . . . . . . . 10 (𝑀𝑉 → (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = (𝑖 / 𝑥𝐵𝐶))
7271eqeq1d 2820 . . . . . . . . 9 (𝑀𝑉 → ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (𝑖 / 𝑥𝐵𝐶) = ∅))
7372ralbidv 3194 . . . . . . . 8 (𝑀𝑉 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅))
7458, 67, 733bitr4d 312 . . . . . . 7 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
7574adantr 481 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
7648, 75bitr4d 283 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅))
7776anbi2d 628 . . . 4 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
78 orcom 864 . . . . . . . 8 (((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
7978ralbii 3162 . . . . . . 7 (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
80 r19.30 3335 . . . . . . . 8 (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗))
81 clel5 3654 . . . . . . . . . . 11 (𝑀𝐴 ↔ ∃𝑗𝐴 𝑀 = 𝑗)
82 biorf 930 . . . . . . . . . . 11 (¬ ∃𝑗𝐴 𝑀 = 𝑗 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
8381, 82sylnbi 331 . . . . . . . . . 10 𝑀𝐴 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
8483adantl 482 . . . . . . . . 9 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
85 orcom 864 . . . . . . . . 9 ((∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗))
8684, 85syl6bb 288 . . . . . . . 8 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗)))
8780, 86syl5ibr 247 . . . . . . 7 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) → ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
8879, 87syl5bir 244 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) → ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
89 olc 862 . . . . . . 7 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
9089ralimi 3157 . . . . . 6 (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
9188, 90impbid1 226 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
92 nfv 1906 . . . . . . . . . 10 𝑗(𝐵𝐶) = ∅
93 nfcsb1v 3904 . . . . . . . . . . . 12 𝑥𝑗 / 𝑥𝐵
9493, 51nfin 4190 . . . . . . . . . . 11 𝑥(𝑗 / 𝑥𝐵𝐶)
9594nfeq1 2990 . . . . . . . . . 10 𝑥(𝑗 / 𝑥𝐵𝐶) = ∅
96 csbeq1a 3894 . . . . . . . . . . . 12 (𝑥 = 𝑗𝐵 = 𝑗 / 𝑥𝐵)
9796ineq1d 4185 . . . . . . . . . . 11 (𝑥 = 𝑗 → (𝐵𝐶) = (𝑗 / 𝑥𝐵𝐶))
9897eqeq1d 2820 . . . . . . . . . 10 (𝑥 = 𝑗 → ((𝐵𝐶) = ∅ ↔ (𝑗 / 𝑥𝐵𝐶) = ∅))
9992, 95, 98cbvralw 3439 . . . . . . . . 9 (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅)
10099a1i 11 . . . . . . . 8 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅))
101 incom 4175 . . . . . . . . . 10 (𝑗 / 𝑥𝐵𝐶) = (𝐶𝑗 / 𝑥𝐵)
102101eqeq1i 2823 . . . . . . . . 9 ((𝑗 / 𝑥𝐵𝐶) = ∅ ↔ (𝐶𝑗 / 𝑥𝐵) = ∅)
103102ralbii 3162 . . . . . . . 8 (∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅)
104100, 103syl6bb 288 . . . . . . 7 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅))
10570ineq1d 4185 . . . . . . . . 9 (𝑀𝑉 → (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝐶𝑗 / 𝑥𝐵))
106105eqeq1d 2820 . . . . . . . 8 (𝑀𝑉 → ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝐶𝑗 / 𝑥𝐵) = ∅))
107106ralbidv 3194 . . . . . . 7 (𝑀𝑉 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅))
108104, 67, 1073bitr4d 312 . . . . . 6 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
109108adantr 481 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
11091, 109bitr4d 283 . . . 4 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅))
11177, 110anbi12d 630 . . 3 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ ((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
112 anass 469 . . . 4 (((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐵 ∧ (( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
113 anidm 565 . . . . 5 ((( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅)
114113anbi2i 622 . . . 4 ((Disj 𝑥𝐴 𝐵 ∧ (( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅))
115112, 114bitri 276 . . 3 (((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅))
116111, 115syl6bb 288 . 2 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
11734, 116bitrd 280 1 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841   = wceq 1528  wcel 2105  wral 3135  wrex 3136  csb 3880  cun 3931  cin 3932  wss 3933  c0 4288  {csn 4557   ciun 4910  Disj wdisj 5022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-sn 4558  df-iun 4912  df-disj 5023
This theorem is referenced by:  disjun0  30273  disjiunel  30274
  Copyright terms: Public domain W3C validator