Metamath Proof Explorer

Theorem disjunsn

Description: Append an element to a disjoint collection. Similar to ralunsn , gsumunsn , etc. (Contributed by Thierry Arnoux, 28-Mar-2018)

Ref Expression
Hypothesis disjunsn.s ⊢x=M→B=C
Assertion disjunsn ⊢M∈V∧¬M∈A→Disjx∈A∪MB↔Disjx∈AB∧⋃x∈AB∩C=∅

Proof

Step Hyp Ref Expression
1 disjunsn.s ⊢x=M→B=C
2 disjors ⊢Disjx∈A∪MB↔∀i∈A∪M∀j∈A∪Mi=j∨⦋i/x⦌B∩⦋j/x⦌B=∅
3 eqeq1 ⊢i=M→i=j↔M=j
4 csbeq1 ⊢i=M→⦋i/x⦌B=⦋M/x⦌B
5 4 ineq1d ⊢i=M→⦋i/x⦌B∩⦋j/x⦌B=⦋M/x⦌B∩⦋j/x⦌B
6 5 eqeq1d ⊢i=M→⦋i/x⦌B∩⦋j/x⦌B=∅↔⦋M/x⦌B∩⦋j/x⦌B=∅
7 3 6 orbi12d ⊢i=M→i=j∨⦋i/x⦌B∩⦋j/x⦌B=∅↔M=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
8 7 ralbidv ⊢i=M→∀j∈A∪Mi=j∨⦋i/x⦌B∩⦋j/x⦌B=∅↔∀j∈A∪MM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
9 8 ralunsn ⊢M∈V→∀i∈A∪M∀j∈A∪Mi=j∨⦋i/x⦌B∩⦋j/x⦌B=∅↔∀i∈A∀j∈A∪Mi=j∨⦋i/x⦌B∩⦋j/x⦌B=∅∧∀j∈A∪MM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
10 2 9 bitrid ⊢M∈V→Disjx∈A∪MB↔∀i∈A∀j∈A∪Mi=j∨⦋i/x⦌B∩⦋j/x⦌B=∅∧∀j∈A∪MM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
11 eqeq2 ⊢j=M→i=j↔i=M
12 csbeq1 ⊢j=M→⦋j/x⦌B=⦋M/x⦌B
13 12 ineq2d ⊢j=M→⦋i/x⦌B∩⦋j/x⦌B=⦋i/x⦌B∩⦋M/x⦌B
14 13 eqeq1d ⊢j=M→⦋i/x⦌B∩⦋j/x⦌B=∅↔⦋i/x⦌B∩⦋M/x⦌B=∅
15 11 14 orbi12d ⊢j=M→i=j∨⦋i/x⦌B∩⦋j/x⦌B=∅↔i=M∨⦋i/x⦌B∩⦋M/x⦌B=∅
16 15 ralunsn ⊢M∈V→∀j∈A∪Mi=j∨⦋i/x⦌B∩⦋j/x⦌B=∅↔∀j∈Ai=j∨⦋i/x⦌B∩⦋j/x⦌B=∅∧i=M∨⦋i/x⦌B∩⦋M/x⦌B=∅
17 16 ralbidv ⊢M∈V→∀i∈A∀j∈A∪Mi=j∨⦋i/x⦌B∩⦋j/x⦌B=∅↔∀i∈A∀j∈Ai=j∨⦋i/x⦌B∩⦋j/x⦌B=∅∧i=M∨⦋i/x⦌B∩⦋M/x⦌B=∅
18 eqeq2 ⊢j=M→M=j↔M=M
19 12 ineq2d ⊢j=M→⦋M/x⦌B∩⦋j/x⦌B=⦋M/x⦌B∩⦋M/x⦌B
20 19 eqeq1d ⊢j=M→⦋M/x⦌B∩⦋j/x⦌B=∅↔⦋M/x⦌B∩⦋M/x⦌B=∅
21 18 20 orbi12d ⊢j=M→M=j∨⦋M/x⦌B∩⦋j/x⦌B=∅↔M=M∨⦋M/x⦌B∩⦋M/x⦌B=∅
22 21 ralunsn ⊢M∈V→∀j∈A∪MM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅↔∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅∧M=M∨⦋M/x⦌B∩⦋M/x⦌B=∅
23 eqid ⊢M=M
24 23 orci ⊢M=M∨⦋M/x⦌B∩⦋M/x⦌B=∅
25 24 biantru ⊢∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅↔∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅∧M=M∨⦋M/x⦌B∩⦋M/x⦌B=∅
26 22 25 bitr4di ⊢M∈V→∀j∈A∪MM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅↔∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
27 17 26 anbi12d ⊢M∈V→∀i∈A∀j∈A∪Mi=j∨⦋i/x⦌B∩⦋j/x⦌B=∅∧∀j∈A∪MM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅↔∀i∈A∀j∈Ai=j∨⦋i/x⦌B∩⦋j/x⦌B=∅∧i=M∨⦋i/x⦌B∩⦋M/x⦌B=∅∧∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
28 10 27 bitrd ⊢M∈V→Disjx∈A∪MB↔∀i∈A∀j∈Ai=j∨⦋i/x⦌B∩⦋j/x⦌B=∅∧i=M∨⦋i/x⦌B∩⦋M/x⦌B=∅∧∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
29 r19.26 ⊢∀i∈A∀j∈Ai=j∨⦋i/x⦌B∩⦋j/x⦌B=∅∧i=M∨⦋i/x⦌B∩⦋M/x⦌B=∅↔∀i∈A∀j∈Ai=j∨⦋i/x⦌B∩⦋j/x⦌B=∅∧∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅
30 disjors ⊢Disjx∈AB↔∀i∈A∀j∈Ai=j∨⦋i/x⦌B∩⦋j/x⦌B=∅
31 30 anbi1i ⊢Disjx∈AB∧∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅↔∀i∈A∀j∈Ai=j∨⦋i/x⦌B∩⦋j/x⦌B=∅∧∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅
32 29 31 bitr4i ⊢∀i∈A∀j∈Ai=j∨⦋i/x⦌B∩⦋j/x⦌B=∅∧i=M∨⦋i/x⦌B∩⦋M/x⦌B=∅↔Disjx∈AB∧∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅
33 32 anbi1i ⊢∀i∈A∀j∈Ai=j∨⦋i/x⦌B∩⦋j/x⦌B=∅∧i=M∨⦋i/x⦌B∩⦋M/x⦌B=∅∧∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅↔Disjx∈AB∧∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅∧∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
34 28 33 bitrdi ⊢M∈V→Disjx∈A∪MB↔Disjx∈AB∧∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅∧∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
35 34 adantr ⊢M∈V∧¬M∈A→Disjx∈A∪MB↔Disjx∈AB∧∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅∧∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
36 orcom ⊢⦋i/x⦌B∩⦋M/x⦌B=∅∨i=M↔i=M∨⦋i/x⦌B∩⦋M/x⦌B=∅
37 36 ralbii ⊢∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅∨i=M↔∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅
38 r19.30 ⊢∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅∨i=M→∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅∨∃i∈Ai=M
39 risset ⊢M∈A↔∃i∈Ai=M
40 biorf ⊢¬∃i∈Ai=M→∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅↔∃i∈Ai=M∨∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅
41 39 40 sylnbi ⊢¬M∈A→∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅↔∃i∈Ai=M∨∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅
42 41 adantl ⊢M∈V∧¬M∈A→∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅↔∃i∈Ai=M∨∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅
43 orcom ⊢∃i∈Ai=M∨∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅↔∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅∨∃i∈Ai=M
44 42 43 bitrdi ⊢M∈V∧¬M∈A→∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅↔∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅∨∃i∈Ai=M
45 38 44 imbitrrid ⊢M∈V∧¬M∈A→∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅∨i=M→∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅
46 37 45 biimtrrid ⊢M∈V∧¬M∈A→∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅→∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅
47 olc ⊢⦋i/x⦌B∩⦋M/x⦌B=∅→i=M∨⦋i/x⦌B∩⦋M/x⦌B=∅
48 47 ralimi ⊢∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅→∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅
49 46 48 impbid1 ⊢M∈V∧¬M∈A→∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅↔∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅
50 nfv ⊢ℲiB∩C=∅
51 nfcsb1v ⊢Ⅎ_x⦋i/x⦌B
52 nfcv ⊢Ⅎ_xC
53 51 52 nfin ⊢Ⅎ_x⦋i/x⦌B∩C
54 53 nfeq1 ⊢Ⅎx⦋i/x⦌B∩C=∅
55 csbeq1a ⊢x=i→B=⦋i/x⦌B
56 55 ineq1d ⊢x=i→B∩C=⦋i/x⦌B∩C
57 56 eqeq1d ⊢x=i→B∩C=∅↔⦋i/x⦌B∩C=∅
58 50 54 57 cbvralw ⊢∀x∈AB∩C=∅↔∀i∈A⦋i/x⦌B∩C=∅
59 58 a1i ⊢M∈V→∀x∈AB∩C=∅↔∀i∈A⦋i/x⦌B∩C=∅
60 ss0b ⊢⋃x∈AB∩C⊆∅↔⋃x∈AB∩C=∅
61 iunss ⊢⋃x∈AB∩C⊆∅↔∀x∈AB∩C⊆∅
62 iunin1 ⊢⋃x∈AB∩C=⋃x∈AB∩C
63 62 eqeq1i ⊢⋃x∈AB∩C=∅↔⋃x∈AB∩C=∅
64 60 61 63 3bitr3ri ⊢⋃x∈AB∩C=∅↔∀x∈AB∩C⊆∅
65 ss0b ⊢B∩C⊆∅↔B∩C=∅
66 65 ralbii ⊢∀x∈AB∩C⊆∅↔∀x∈AB∩C=∅
67 64 66 bitri ⊢⋃x∈AB∩C=∅↔∀x∈AB∩C=∅
68 67 a1i ⊢M∈V→⋃x∈AB∩C=∅↔∀x∈AB∩C=∅
69 nfcvd ⊢M∈V→Ⅎ_xC
70 69 1 csbiegf ⊢M∈V→⦋M/x⦌B=C
71 70 ineq2d ⊢M∈V→⦋i/x⦌B∩⦋M/x⦌B=⦋i/x⦌B∩C
72 71 eqeq1d ⊢M∈V→⦋i/x⦌B∩⦋M/x⦌B=∅↔⦋i/x⦌B∩C=∅
73 72 ralbidv ⊢M∈V→∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅↔∀i∈A⦋i/x⦌B∩C=∅
74 59 68 73 3bitr4d ⊢M∈V→⋃x∈AB∩C=∅↔∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅
75 74 adantr ⊢M∈V∧¬M∈A→⋃x∈AB∩C=∅↔∀i∈A⦋i/x⦌B∩⦋M/x⦌B=∅
76 49 75 bitr4d ⊢M∈V∧¬M∈A→∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅↔⋃x∈AB∩C=∅
77 76 anbi2d ⊢M∈V∧¬M∈A→Disjx∈AB∧∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅↔Disjx∈AB∧⋃x∈AB∩C=∅
78 orcom ⊢⦋M/x⦌B∩⦋j/x⦌B=∅∨M=j↔M=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
79 78 ralbii ⊢∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅∨M=j↔∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
80 r19.30 ⊢∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅∨M=j→∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅∨∃j∈AM=j
81 clel5 ⊢M∈A↔∃j∈AM=j
82 biorf ⊢¬∃j∈AM=j→∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅↔∃j∈AM=j∨∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅
83 81 82 sylnbi ⊢¬M∈A→∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅↔∃j∈AM=j∨∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅
84 83 adantl ⊢M∈V∧¬M∈A→∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅↔∃j∈AM=j∨∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅
85 orcom ⊢∃j∈AM=j∨∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅↔∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅∨∃j∈AM=j
86 84 85 bitrdi ⊢M∈V∧¬M∈A→∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅↔∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅∨∃j∈AM=j
87 80 86 imbitrrid ⊢M∈V∧¬M∈A→∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅∨M=j→∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅
88 79 87 biimtrrid ⊢M∈V∧¬M∈A→∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅→∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅
89 olc ⊢⦋M/x⦌B∩⦋j/x⦌B=∅→M=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
90 89 ralimi ⊢∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅→∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅
91 88 90 impbid1 ⊢M∈V∧¬M∈A→∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅↔∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅
92 nfv ⊢ℲjB∩C=∅
93 nfcsb1v ⊢Ⅎ_x⦋j/x⦌B
94 93 52 nfin ⊢Ⅎ_x⦋j/x⦌B∩C
95 94 nfeq1 ⊢Ⅎx⦋j/x⦌B∩C=∅
96 csbeq1a ⊢x=j→B=⦋j/x⦌B
97 96 ineq1d ⊢x=j→B∩C=⦋j/x⦌B∩C
98 97 eqeq1d ⊢x=j→B∩C=∅↔⦋j/x⦌B∩C=∅
99 92 95 98 cbvralw ⊢∀x∈AB∩C=∅↔∀j∈A⦋j/x⦌B∩C=∅
100 99 a1i ⊢M∈V→∀x∈AB∩C=∅↔∀j∈A⦋j/x⦌B∩C=∅
101 incom ⊢⦋j/x⦌B∩C=C∩⦋j/x⦌B
102 101 eqeq1i ⊢⦋j/x⦌B∩C=∅↔C∩⦋j/x⦌B=∅
103 102 ralbii ⊢∀j∈A⦋j/x⦌B∩C=∅↔∀j∈AC∩⦋j/x⦌B=∅
104 100 103 bitrdi ⊢M∈V→∀x∈AB∩C=∅↔∀j∈AC∩⦋j/x⦌B=∅
105 70 ineq1d ⊢M∈V→⦋M/x⦌B∩⦋j/x⦌B=C∩⦋j/x⦌B
106 105 eqeq1d ⊢M∈V→⦋M/x⦌B∩⦋j/x⦌B=∅↔C∩⦋j/x⦌B=∅
107 106 ralbidv ⊢M∈V→∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅↔∀j∈AC∩⦋j/x⦌B=∅
108 104 68 107 3bitr4d ⊢M∈V→⋃x∈AB∩C=∅↔∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅
109 108 adantr ⊢M∈V∧¬M∈A→⋃x∈AB∩C=∅↔∀j∈A⦋M/x⦌B∩⦋j/x⦌B=∅
110 91 109 bitr4d ⊢M∈V∧¬M∈A→∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅↔⋃x∈AB∩C=∅
111 77 110 anbi12d ⊢M∈V∧¬M∈A→Disjx∈AB∧∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅∧∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅↔Disjx∈AB∧⋃x∈AB∩C=∅∧⋃x∈AB∩C=∅
112 anass ⊢Disjx∈AB∧⋃x∈AB∩C=∅∧⋃x∈AB∩C=∅↔Disjx∈AB∧⋃x∈AB∩C=∅∧⋃x∈AB∩C=∅
113 anidm ⊢⋃x∈AB∩C=∅∧⋃x∈AB∩C=∅↔⋃x∈AB∩C=∅
114 113 anbi2i ⊢Disjx∈AB∧⋃x∈AB∩C=∅∧⋃x∈AB∩C=∅↔Disjx∈AB∧⋃x∈AB∩C=∅
115 112 114 bitri ⊢Disjx∈AB∧⋃x∈AB∩C=∅∧⋃x∈AB∩C=∅↔Disjx∈AB∧⋃x∈AB∩C=∅
116 111 115 bitrdi ⊢M∈V∧¬M∈A→Disjx∈AB∧∀i∈Ai=M∨⦋i/x⦌B∩⦋M/x⦌B=∅∧∀j∈AM=j∨⦋M/x⦌B∩⦋j/x⦌B=∅↔Disjx∈AB∧⋃x∈AB∩C=∅
117 35 116 bitrd ⊢M∈V∧¬M∈A→Disjx∈A∪MB↔Disjx∈AB∧⋃x∈AB∩C=∅