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 Disj x A M B Disj x A B x A B C =

Proof

Step Hyp Ref Expression
1 disjunsn.s x = M B = C
2 disjors Disj x A M B i A M j A M i = 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 M i = j i / x B j / x B = j A M M = j M / x B j / x B =
9 8 ralunsn M V i A M j A M i = j i / x B j / x B = i A j A M i = j i / x B j / x B = j A M M = j M / x B j / x B =
10 2 9 syl5bb M V Disj x A M B i A j A M i = j i / x B j / x B = j A M M = 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 M i = j i / x B j / x B = j A i = j i / x B j / x B = i = M i / x B M / x B =
17 16 ralbidv M V i A j A M i = j i / x B j / x B = i A j A i = 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 M M = j M / x B j / x B = j A M = 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 A M = j M / x B j / x B = j A M = j M / x B j / x B = M = M M / x B M / x B =
26 22 25 bitr4di M V j A M M = j M / x B j / x B = j A M = j M / x B j / x B =
27 17 26 anbi12d M V i A j A M i = j i / x B j / x B = j A M M = j M / x B j / x B = i A j A i = j i / x B j / x B = i = M i / x B M / x B = j A M = j M / x B j / x B =
28 10 27 bitrd M V Disj x A M B i A j A i = j i / x B j / x B = i = M i / x B M / x B = j A M = j M / x B j / x B =
29 r19.26 i A j A i = j i / x B j / x B = i = M i / x B M / x B = i A j A i = j i / x B j / x B = i A i = M i / x B M / x B =
30 disjors Disj x A B i A j A i = j i / x B j / x B =
31 30 anbi1i Disj x A B i A i = M i / x B M / x B = i A j A i = j i / x B j / x B = i A i = M i / x B M / x B =
32 29 31 bitr4i i A j A i = j i / x B j / x B = i = M i / x B M / x B = Disj x A B i A i = M i / x B M / x B =
33 32 anbi1i i A j A i = j i / x B j / x B = i = M i / x B M / x B = j A M = j M / x B j / x B = Disj x A B i A i = M i / x B M / x B = j A M = j M / x B j / x B =
34 28 33 bitrdi M V Disj x A M B Disj x A B i A i = M i / x B M / x B = j A M = j M / x B j / x B =
35 34 adantr M V ¬ M A Disj x A M B Disj x A B i A i = M i / x B M / x B = j A M = 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 A i = 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 A i = M
39 risset M A i A i = M
40 biorf ¬ i A i = M i A i / x B M / x B = i A i = M i A i / x B M / x B =
41 39 40 sylnbi ¬ M A i A i / x B M / x B = i A i = 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 A i = M i A i / x B M / x B =
43 orcom i A i = M i A i / x B M / x B = i A i / x B M / x B = i A i = 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 A i = M
45 38 44 syl5ibr 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 syl5bir M V ¬ M A i A i = 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 A i = M i / x B M / x B =
49 46 48 impbid1 M V ¬ M A i A i = M i / x B M / x B = i A i / x B M / x B =
50 nfv i B C =
51 nfcsb1v _ x i / x B
52 nfcv _ x C
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 A B C = i A i / x B C =
59 58 a1i M V x A B C = i A i / x B C =
60 ss0b x A B C x A B C =
61 iunss x A B C x A B C
62 iunin1 x A B C = x A B C
63 62 eqeq1i x A B C = x A B C =
64 60 61 63 3bitr3ri x A B C = x A B C
65 ss0b B C B C =
66 65 ralbii x A B C x A B C =
67 64 66 bitri x A B C = x A B C =
68 67 a1i M V x A B C = x A B C =
69 nfcvd M V _ x C
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 A B C = i A i / x B M / x B =
75 74 adantr M V ¬ M A x A B C = i A i / x B M / x B =
76 49 75 bitr4d M V ¬ M A i A i = M i / x B M / x B = x A B C =
77 76 anbi2d M V ¬ M A Disj x A B i A i = M i / x B M / x B = Disj x A B x A B 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 A M = 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 A M = j
81 clel5 M A j A M = j
82 biorf ¬ j A M = j j A M / x B j / x B = j A M = j j A M / x B j / x B =
83 81 82 sylnbi ¬ M A j A M / x B j / x B = j A M = 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 A M = j j A M / x B j / x B =
85 orcom j A M = j j A M / x B j / x B = j A M / x B j / x B = j A M = 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 A M = j
87 80 86 syl5ibr 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 syl5bir M V ¬ M A j A M = 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 A M = j M / x B j / x B =
91 88 90 impbid1 M V ¬ M A j A M = j M / x B j / x B = j A M / x B j / x B =
92 nfv j B 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 A B C = j A j / x B C =
100 99 a1i M V x A B 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 A C j / x B =
104 100 103 bitrdi M V x A B C = j A C 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 A C j / x B =
108 104 68 107 3bitr4d M V x A B C = j A M / x B j / x B =
109 108 adantr M V ¬ M A x A B C = j A M / x B j / x B =
110 91 109 bitr4d M V ¬ M A j A M = j M / x B j / x B = x A B C =
111 77 110 anbi12d M V ¬ M A Disj x A B i A i = M i / x B M / x B = j A M = j M / x B j / x B = Disj x A B x A B C = x A B C =
112 anass Disj x A B x A B C = x A B C = Disj x A B x A B C = x A B C =
113 anidm x A B C = x A B C = x A B C =
114 113 anbi2i Disj x A B x A B C = x A B C = Disj x A B x A B C =
115 112 114 bitri Disj x A B x A B C = x A B C = Disj x A B x A B C =
116 111 115 bitrdi M V ¬ M A Disj x A B i A i = M i / x B M / x B = j A M = j M / x B j / x B = Disj x A B x A B C =
117 35 116 bitrd M V ¬ M A Disj x A M B Disj x A B x A B C =