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

Theorem disjunsn 28789
 Description: Append an element to a disjoint collection. Similar to ralunsn 4360, gsumunsn 18182, 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 4568 . . . . . 6 (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
2 eqeq1 2614 . . . . . . . . 9 (𝑖 = 𝑀 → (𝑖 = 𝑗𝑀 = 𝑗))
3 csbeq1 3502 . . . . . . . . . . 11 (𝑖 = 𝑀𝑖 / 𝑥𝐵 = 𝑀 / 𝑥𝐵)
43ineq1d 3775 . . . . . . . . . 10 (𝑖 = 𝑀 → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵))
54eqeq1d 2612 . . . . . . . . 9 (𝑖 = 𝑀 → ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
62, 5orbi12d 742 . . . . . . . 8 (𝑖 = 𝑀 → ((𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
76ralbidv 2969 . . . . . . 7 (𝑖 = 𝑀 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
87ralunsn 4360 . . . . . 6 (𝑀𝑉 → (∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
91, 8syl5bb 271 . . . . 5 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
10 eqeq2 2621 . . . . . . . . 9 (𝑗 = 𝑀 → (𝑖 = 𝑗𝑖 = 𝑀))
11 csbeq1 3502 . . . . . . . . . . 11 (𝑗 = 𝑀𝑗 / 𝑥𝐵 = 𝑀 / 𝑥𝐵)
1211ineq2d 3776 . . . . . . . . . 10 (𝑗 = 𝑀 → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵))
1312eqeq1d 2612 . . . . . . . . 9 (𝑗 = 𝑀 → ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
1410, 13orbi12d 742 . . . . . . . 8 (𝑗 = 𝑀 → ((𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
1514ralunsn 4360 . . . . . . 7 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
1615ralbidv 2969 . . . . . 6 (𝑀𝑉 → (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
17 eqeq2 2621 . . . . . . . . 9 (𝑗 = 𝑀 → (𝑀 = 𝑗𝑀 = 𝑀))
1811ineq2d 3776 . . . . . . . . . 10 (𝑗 = 𝑀 → (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵))
1918eqeq1d 2612 . . . . . . . . 9 (𝑗 = 𝑀 → ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
2017, 19orbi12d 742 . . . . . . . 8 (𝑗 = 𝑀 → ((𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
2120ralunsn 4360 . . . . . . 7 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
22 eqid 2610 . . . . . . . . 9 𝑀 = 𝑀
2322orci 404 . . . . . . . 8 (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)
2423biantru 525 . . . . . . 7 (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
2521, 24syl6bbr 277 . . . . . 6 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
2616, 25anbi12d 743 . . . . 5 (𝑀𝑉 → ((∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
279, 26bitrd 267 . . . 4 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
28 r19.26 3046 . . . . . 6 (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
29 disjors 4568 . . . . . . 7 (Disj 𝑥𝐴 𝐵 ↔ ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
3029anbi1i 727 . . . . . 6 ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
3128, 30bitr4i 266 . . . . 5 (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
3231anbi1i 727 . . . 4 ((∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
3327, 32syl6bb 275 . . 3 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
3433adantr 480 . 2 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
35 orcom 401 . . . . . . . . 9 (((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
3635ralbii 2963 . . . . . . . 8 (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
37 r19.30 3063 . . . . . . . . 9 (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀))
38 risset 3044 . . . . . . . . . . . 12 (𝑀𝐴 ↔ ∃𝑖𝐴 𝑖 = 𝑀)
39 biorf 419 . . . . . . . . . . . 12 (¬ ∃𝑖𝐴 𝑖 = 𝑀 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
4038, 39sylnbi 319 . . . . . . . . . . 11 𝑀𝐴 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
4140adantl 481 . . . . . . . . . 10 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
42 orcom 401 . . . . . . . . . 10 ((∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀))
4341, 42syl6bb 275 . . . . . . . . 9 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀)))
4437, 43syl5ibr 235 . . . . . . . 8 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) → ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4536, 44syl5bir 232 . . . . . . 7 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) → ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
46 olc 398 . . . . . . . 8 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ → (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4746ralimi 2936 . . . . . . 7 (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ → ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4845, 47impbid1 214 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
49 nfv 1830 . . . . . . . . . 10 𝑖(𝐵𝐶) = ∅
50 nfcsb1v 3515 . . . . . . . . . . . 12 𝑥𝑖 / 𝑥𝐵
51 nfcv 2751 . . . . . . . . . . . 12 𝑥𝐶
5250, 51nfin 3782 . . . . . . . . . . 11 𝑥(𝑖 / 𝑥𝐵𝐶)
5352nfeq1 2764 . . . . . . . . . 10 𝑥(𝑖 / 𝑥𝐵𝐶) = ∅
54 csbeq1a 3508 . . . . . . . . . . . 12 (𝑥 = 𝑖𝐵 = 𝑖 / 𝑥𝐵)
5554ineq1d 3775 . . . . . . . . . . 11 (𝑥 = 𝑖 → (𝐵𝐶) = (𝑖 / 𝑥𝐵𝐶))
5655eqeq1d 2612 . . . . . . . . . 10 (𝑥 = 𝑖 → ((𝐵𝐶) = ∅ ↔ (𝑖 / 𝑥𝐵𝐶) = ∅))
5749, 53, 56cbvral 3143 . . . . . . . . 9 (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅)
5857a1i 11 . . . . . . . 8 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅))
59 ss0b 3925 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ 𝑥𝐴 (𝐵𝐶) = ∅)
60 iunss 4497 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) ⊆ ∅)
61 iunin1 4521 . . . . . . . . . . . 12 𝑥𝐴 (𝐵𝐶) = ( 𝑥𝐴 𝐵𝐶)
6261eqeq1i 2615 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) = ∅ ↔ ( 𝑥𝐴 𝐵𝐶) = ∅)
6359, 60, 623bitr3ri 290 . . . . . . . . . 10 (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) ⊆ ∅)
64 ss0b 3925 . . . . . . . . . . 11 ((𝐵𝐶) ⊆ ∅ ↔ (𝐵𝐶) = ∅)
6564ralbii 2963 . . . . . . . . . 10 (∀𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅)
6663, 65bitri 263 . . . . . . . . 9 (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅)
6766a1i 11 . . . . . . . 8 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅))
68 nfcvd 2752 . . . . . . . . . . . 12 (𝑀𝑉𝑥𝐶)
69 disjunsn.s . . . . . . . . . . . 12 (𝑥 = 𝑀𝐵 = 𝐶)
7068, 69csbiegf 3523 . . . . . . . . . . 11 (𝑀𝑉𝑀 / 𝑥𝐵 = 𝐶)
7170ineq2d 3776 . . . . . . . . . 10 (𝑀𝑉 → (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = (𝑖 / 𝑥𝐵𝐶))
7271eqeq1d 2612 . . . . . . . . 9 (𝑀𝑉 → ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (𝑖 / 𝑥𝐵𝐶) = ∅))
7372ralbidv 2969 . . . . . . . 8 (𝑀𝑉 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅))
7458, 67, 733bitr4d 299 . . . . . . 7 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
7574adantr 480 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
7648, 75bitr4d 270 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅))
7776anbi2d 736 . . . 4 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
78 orcom 401 . . . . . . . 8 (((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
7978ralbii 2963 . . . . . . 7 (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
80 r19.30 3063 . . . . . . . 8 (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗))
81 risset 3044 . . . . . . . . . . . 12 (𝑀𝐴 ↔ ∃𝑗𝐴 𝑗 = 𝑀)
82 eqcom 2617 . . . . . . . . . . . . 13 (𝑗 = 𝑀𝑀 = 𝑗)
8382rexbii 3023 . . . . . . . . . . . 12 (∃𝑗𝐴 𝑗 = 𝑀 ↔ ∃𝑗𝐴 𝑀 = 𝑗)
8481, 83bitri 263 . . . . . . . . . . 11 (𝑀𝐴 ↔ ∃𝑗𝐴 𝑀 = 𝑗)
85 biorf 419 . . . . . . . . . . 11 (¬ ∃𝑗𝐴 𝑀 = 𝑗 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
8684, 85sylnbi 319 . . . . . . . . . 10 𝑀𝐴 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
8786adantl 481 . . . . . . . . 9 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
88 orcom 401 . . . . . . . . 9 ((∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗))
8987, 88syl6bb 275 . . . . . . . 8 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗)))
9080, 89syl5ibr 235 . . . . . . 7 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) → ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
9179, 90syl5bir 232 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) → ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
92 olc 398 . . . . . . 7 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
9392ralimi 2936 . . . . . 6 (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
9491, 93impbid1 214 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
95 nfv 1830 . . . . . . . . . 10 𝑗(𝐵𝐶) = ∅
96 nfcsb1v 3515 . . . . . . . . . . . 12 𝑥𝑗 / 𝑥𝐵
9796, 51nfin 3782 . . . . . . . . . . 11 𝑥(𝑗 / 𝑥𝐵𝐶)
9897nfeq1 2764 . . . . . . . . . 10 𝑥(𝑗 / 𝑥𝐵𝐶) = ∅
99 csbeq1a 3508 . . . . . . . . . . . 12 (𝑥 = 𝑗𝐵 = 𝑗 / 𝑥𝐵)
10099ineq1d 3775 . . . . . . . . . . 11 (𝑥 = 𝑗 → (𝐵𝐶) = (𝑗 / 𝑥𝐵𝐶))
101100eqeq1d 2612 . . . . . . . . . 10 (𝑥 = 𝑗 → ((𝐵𝐶) = ∅ ↔ (𝑗 / 𝑥𝐵𝐶) = ∅))
10295, 98, 101cbvral 3143 . . . . . . . . 9 (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅)
103102a1i 11 . . . . . . . 8 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅))
104 incom 3767 . . . . . . . . . 10 (𝑗 / 𝑥𝐵𝐶) = (𝐶𝑗 / 𝑥𝐵)
105104eqeq1i 2615 . . . . . . . . 9 ((𝑗 / 𝑥𝐵𝐶) = ∅ ↔ (𝐶𝑗 / 𝑥𝐵) = ∅)
106105ralbii 2963 . . . . . . . 8 (∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅)
107103, 106syl6bb 275 . . . . . . 7 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅))
10870ineq1d 3775 . . . . . . . . 9 (𝑀𝑉 → (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝐶𝑗 / 𝑥𝐵))
109108eqeq1d 2612 . . . . . . . 8 (𝑀𝑉 → ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝐶𝑗 / 𝑥𝐵) = ∅))
110109ralbidv 2969 . . . . . . 7 (𝑀𝑉 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅))
111107, 67, 1103bitr4d 299 . . . . . 6 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
112111adantr 480 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
11394, 112bitr4d 270 . . . 4 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅))
11477, 113anbi12d 743 . . 3 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ ((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
115 anass 679 . . . 4 (((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐵 ∧ (( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
116 anidm 674 . . . . 5 ((( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅)
117116anbi2i 726 . . . 4 ((Disj 𝑥𝐴 𝐵 ∧ (( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅))
118115, 117bitri 263 . . 3 (((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅))
119114, 118syl6bb 275 . 2 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
12034, 119bitrd 267 1 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  ⦋csb 3499   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  {csn 4125  ∪ 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-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-sn 4126  df-iun 4457  df-disj 4554 This theorem is referenced by:  disjun0  28790  disjiunel  28791
 Copyright terms: Public domain W3C validator