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 32377
Description: Append an element to a disjoint collection. Similar to ralunsn 4890, gsumunsn 19908, 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 5123 . . . . . 6 (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
2 eqeq1 2731 . . . . . . . . 9 (𝑖 = 𝑀 → (𝑖 = 𝑗𝑀 = 𝑗))
3 csbeq1 3892 . . . . . . . . . . 11 (𝑖 = 𝑀𝑖 / 𝑥𝐵 = 𝑀 / 𝑥𝐵)
43ineq1d 4207 . . . . . . . . . 10 (𝑖 = 𝑀 → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵))
54eqeq1d 2729 . . . . . . . . 9 (𝑖 = 𝑀 → ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
62, 5orbi12d 917 . . . . . . . 8 (𝑖 = 𝑀 → ((𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
76ralbidv 3172 . . . . . . 7 (𝑖 = 𝑀 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
87ralunsn 4890 . . . . . 6 (𝑀𝑉 → (∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
91, 8bitrid 283 . . . . 5 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
10 eqeq2 2739 . . . . . . . . 9 (𝑗 = 𝑀 → (𝑖 = 𝑗𝑖 = 𝑀))
11 csbeq1 3892 . . . . . . . . . . 11 (𝑗 = 𝑀𝑗 / 𝑥𝐵 = 𝑀 / 𝑥𝐵)
1211ineq2d 4208 . . . . . . . . . 10 (𝑗 = 𝑀 → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵))
1312eqeq1d 2729 . . . . . . . . 9 (𝑗 = 𝑀 → ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
1410, 13orbi12d 917 . . . . . . . 8 (𝑗 = 𝑀 → ((𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
1514ralunsn 4890 . . . . . . 7 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
1615ralbidv 3172 . . . . . 6 (𝑀𝑉 → (∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
17 eqeq2 2739 . . . . . . . . 9 (𝑗 = 𝑀 → (𝑀 = 𝑗𝑀 = 𝑀))
1811ineq2d 4208 . . . . . . . . . 10 (𝑗 = 𝑀 → (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵))
1918eqeq1d 2729 . . . . . . . . 9 (𝑗 = 𝑀 → ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
2017, 19orbi12d 917 . . . . . . . 8 (𝑗 = 𝑀 → ((𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
2120ralunsn 4890 . . . . . . 7 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))))
22 eqid 2727 . . . . . . . . 9 𝑀 = 𝑀
2322orci 864 . . . . . . . 8 (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)
2423biantru 529 . . . . . . 7 (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (𝑀 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
2521, 24bitr4di 289 . . . . . 6 (𝑀𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
2616, 25anbi12d 630 . . . . 5 (𝑀𝑉 → ((∀𝑖𝐴𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
279, 26bitrd 279 . . . 4 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
28 r19.26 3106 . . . . . 6 (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
29 disjors 5123 . . . . . . 7 (Disj 𝑥𝐴 𝐵 ↔ ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
3029anbi1i 623 . . . . . 6 ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
3128, 30bitr4i 278 . . . . 5 (∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
3231anbi1i 623 . . . 4 ((∀𝑖𝐴 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
3327, 32bitrdi 287 . . 3 (𝑀𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
3433adantr 480 . 2 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))))
35 orcom 869 . . . . . . . . 9 (((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
3635ralbii 3088 . . . . . . . 8 (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
37 r19.30 3115 . . . . . . . . 9 (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀))
38 risset 3225 . . . . . . . . . . . 12 (𝑀𝐴 ↔ ∃𝑖𝐴 𝑖 = 𝑀)
39 biorf 935 . . . . . . . . . . . 12 (¬ ∃𝑖𝐴 𝑖 = 𝑀 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
4038, 39sylnbi 330 . . . . . . . . . . 11 𝑀𝐴 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
4140adantl 481 . . . . . . . . . 10 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)))
42 orcom 869 . . . . . . . . . 10 ((∃𝑖𝐴 𝑖 = 𝑀 ∨ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀))
4341, 42bitrdi 287 . . . . . . . . 9 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ ∃𝑖𝐴 𝑖 = 𝑀)))
4437, 43imbitrrid 245 . . . . . . . 8 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ∨ 𝑖 = 𝑀) → ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4536, 44biimtrrid 242 . . . . . . 7 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) → ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
46 olc 867 . . . . . . . 8 ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ → (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4746ralimi 3078 . . . . . . 7 (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ → ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
4845, 47impbid1 224 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
49 nfv 1910 . . . . . . . . . 10 𝑖(𝐵𝐶) = ∅
50 nfcsb1v 3914 . . . . . . . . . . . 12 𝑥𝑖 / 𝑥𝐵
51 nfcv 2898 . . . . . . . . . . . 12 𝑥𝐶
5250, 51nfin 4212 . . . . . . . . . . 11 𝑥(𝑖 / 𝑥𝐵𝐶)
5352nfeq1 2913 . . . . . . . . . 10 𝑥(𝑖 / 𝑥𝐵𝐶) = ∅
54 csbeq1a 3903 . . . . . . . . . . . 12 (𝑥 = 𝑖𝐵 = 𝑖 / 𝑥𝐵)
5554ineq1d 4207 . . . . . . . . . . 11 (𝑥 = 𝑖 → (𝐵𝐶) = (𝑖 / 𝑥𝐵𝐶))
5655eqeq1d 2729 . . . . . . . . . 10 (𝑥 = 𝑖 → ((𝐵𝐶) = ∅ ↔ (𝑖 / 𝑥𝐵𝐶) = ∅))
5749, 53, 56cbvralw 3298 . . . . . . . . 9 (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅)
5857a1i 11 . . . . . . . 8 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅))
59 ss0b 4393 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ 𝑥𝐴 (𝐵𝐶) = ∅)
60 iunss 5042 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) ⊆ ∅)
61 iunin1 5069 . . . . . . . . . . . 12 𝑥𝐴 (𝐵𝐶) = ( 𝑥𝐴 𝐵𝐶)
6261eqeq1i 2732 . . . . . . . . . . 11 ( 𝑥𝐴 (𝐵𝐶) = ∅ ↔ ( 𝑥𝐴 𝐵𝐶) = ∅)
6359, 60, 623bitr3ri 302 . . . . . . . . . 10 (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) ⊆ ∅)
64 ss0b 4393 . . . . . . . . . . 11 ((𝐵𝐶) ⊆ ∅ ↔ (𝐵𝐶) = ∅)
6564ralbii 3088 . . . . . . . . . 10 (∀𝑥𝐴 (𝐵𝐶) ⊆ ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅)
6663, 65bitri 275 . . . . . . . . 9 (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅)
6766a1i 11 . . . . . . . 8 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑥𝐴 (𝐵𝐶) = ∅))
68 nfcvd 2899 . . . . . . . . . . . 12 (𝑀𝑉𝑥𝐶)
69 disjunsn.s . . . . . . . . . . . 12 (𝑥 = 𝑀𝐵 = 𝐶)
7068, 69csbiegf 3923 . . . . . . . . . . 11 (𝑀𝑉𝑀 / 𝑥𝐵 = 𝐶)
7170ineq2d 4208 . . . . . . . . . 10 (𝑀𝑉 → (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = (𝑖 / 𝑥𝐵𝐶))
7271eqeq1d 2729 . . . . . . . . 9 (𝑀𝑉 → ((𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ (𝑖 / 𝑥𝐵𝐶) = ∅))
7372ralbidv 3172 . . . . . . . 8 (𝑀𝑉 → (∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝐶) = ∅))
7458, 67, 733bitr4d 311 . . . . . . 7 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
7574adantr 480 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑖𝐴 (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅))
7648, 75bitr4d 282 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅))
7776anbi2d 628 . . . 4 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → ((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
78 orcom 869 . . . . . . . 8 (((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
7978ralbii 3088 . . . . . . 7 (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
80 r19.30 3115 . . . . . . . 8 (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗))
81 clel5 3651 . . . . . . . . . . 11 (𝑀𝐴 ↔ ∃𝑗𝐴 𝑀 = 𝑗)
82 biorf 935 . . . . . . . . . . 11 (¬ ∃𝑗𝐴 𝑀 = 𝑗 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
8381, 82sylnbi 330 . . . . . . . . . 10 𝑀𝐴 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
8483adantl 481 . . . . . . . . 9 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)))
85 orcom 869 . . . . . . . . 9 ((∃𝑗𝐴 𝑀 = 𝑗 ∨ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗))
8684, 85bitrdi 287 . . . . . . . 8 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ ∃𝑗𝐴 𝑀 = 𝑗)))
8780, 86imbitrrid 245 . . . . . . 7 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∨ 𝑀 = 𝑗) → ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
8879, 87biimtrrid 242 . . . . . 6 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) → ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
89 olc 867 . . . . . . 7 ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
9089ralimi 3078 . . . . . 6 (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
9188, 90impbid1 224 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
92 nfv 1910 . . . . . . . . . 10 𝑗(𝐵𝐶) = ∅
93 nfcsb1v 3914 . . . . . . . . . . . 12 𝑥𝑗 / 𝑥𝐵
9493, 51nfin 4212 . . . . . . . . . . 11 𝑥(𝑗 / 𝑥𝐵𝐶)
9594nfeq1 2913 . . . . . . . . . 10 𝑥(𝑗 / 𝑥𝐵𝐶) = ∅
96 csbeq1a 3903 . . . . . . . . . . . 12 (𝑥 = 𝑗𝐵 = 𝑗 / 𝑥𝐵)
9796ineq1d 4207 . . . . . . . . . . 11 (𝑥 = 𝑗 → (𝐵𝐶) = (𝑗 / 𝑥𝐵𝐶))
9897eqeq1d 2729 . . . . . . . . . 10 (𝑥 = 𝑗 → ((𝐵𝐶) = ∅ ↔ (𝑗 / 𝑥𝐵𝐶) = ∅))
9992, 95, 98cbvralw 3298 . . . . . . . . 9 (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅)
10099a1i 11 . . . . . . . 8 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅))
101 incom 4197 . . . . . . . . . 10 (𝑗 / 𝑥𝐵𝐶) = (𝐶𝑗 / 𝑥𝐵)
102101eqeq1i 2732 . . . . . . . . 9 ((𝑗 / 𝑥𝐵𝐶) = ∅ ↔ (𝐶𝑗 / 𝑥𝐵) = ∅)
103102ralbii 3088 . . . . . . . 8 (∀𝑗𝐴 (𝑗 / 𝑥𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅)
104100, 103bitrdi 287 . . . . . . 7 (𝑀𝑉 → (∀𝑥𝐴 (𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅))
10570ineq1d 4207 . . . . . . . . 9 (𝑀𝑉 → (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = (𝐶𝑗 / 𝑥𝐵))
106105eqeq1d 2729 . . . . . . . 8 (𝑀𝑉 → ((𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ (𝐶𝑗 / 𝑥𝐵) = ∅))
107106ralbidv 3172 . . . . . . 7 (𝑀𝑉 → (∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ ∀𝑗𝐴 (𝐶𝑗 / 𝑥𝐵) = ∅))
108104, 67, 1073bitr4d 311 . . . . . 6 (𝑀𝑉 → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
109108adantr 480 . . . . 5 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (( 𝑥𝐴 𝐵𝐶) = ∅ ↔ ∀𝑗𝐴 (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
11091, 109bitr4d 282 . . . 4 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅))
11177, 110anbi12d 630 . . 3 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ ((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
112 anass 468 . . . 4 (((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐵 ∧ (( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
113 anidm 564 . . . . 5 ((( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ ( 𝑥𝐴 𝐵𝐶) = ∅)
114113anbi2i 622 . . . 4 ((Disj 𝑥𝐴 𝐵 ∧ (( 𝑥𝐴 𝐵𝐶) = ∅ ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅))
115112, 114bitri 275 . . 3 (((Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ∧ ( 𝑥𝐴 𝐵𝐶) = ∅) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅))
116111, 115bitrdi 287 . 2 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (((Disj 𝑥𝐴 𝐵 ∧ ∀𝑖𝐴 (𝑖 = 𝑀 ∨ (𝑖 / 𝑥𝐵𝑀 / 𝑥𝐵) = ∅)) ∧ ∀𝑗𝐴 (𝑀 = 𝑗 ∨ (𝑀 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
11734, 116bitrd 279 1 ((𝑀𝑉 ∧ ¬ 𝑀𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴 𝐵𝐶) = ∅)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 846   = wceq 1534  wcel 2099  wral 3056  wrex 3065  csb 3889  cun 3942  cin 3943  wss 3944  c0 4318  {csn 4624   ciun 4991  Disj wdisj 5107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ral 3057  df-rex 3066  df-rmo 3371  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-sn 4625  df-iun 4993  df-disj 5108
This theorem is referenced by:  disjun0  32378  disjiunel  32379
  Copyright terms: Public domain W3C validator