Mathbox for Giovanni Mascellani < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mpt2bi123f Structured version   Visualization version   Unicode version

Theorem mpt2bi123f 32399
 Description: Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
Hypotheses
Ref Expression
mpt2bi123f.1
mpt2bi123f.2
mpt2bi123f.3
mpt2bi123f.4
mpt2bi123f.5
mpt2bi123f.6
mpt2bi123f.7
mpt2bi123f.8
Assertion
Ref Expression
mpt2bi123f
Distinct variable group:   ,
Allowed substitution hints:   (,)   (,)   (,)   (,)   (,)   (,)

Proof of Theorem mpt2bi123f
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 mpt2bi123f.1 . . . . . . . 8
2 mpt2bi123f.2 . . . . . . . 8
31, 2nfeq 2602 . . . . . . 7
4 eleq2 2517 . . . . . . 7
53, 4alrimi 1954 . . . . . 6
6 mpt2bi123f.3 . . . . . . . . . 10
76nfcri 2585 . . . . . . . . 9
8 mpt2bi123f.4 . . . . . . . . . 10
98nfcri 2585 . . . . . . . . 9
107, 9nfbi 2016 . . . . . . . 8
11 ax-5 1757 . . . . . . . 8
1210, 11alrimi 1954 . . . . . . 7
1312alimi 1683 . . . . . 6
145, 13syl 17 . . . . 5
15 mpt2bi123f.5 . . . . . . . 8
16 mpt2bi123f.6 . . . . . . . 8
1715, 16nfeq 2602 . . . . . . 7
18 eleq2 2517 . . . . . . 7
1917, 18alrimi 1954 . . . . . 6
20 ax-5 1757 . . . . . . 7
2120alimi 1683 . . . . . 6
22 mpt2bi123f.7 . . . . . . . . . . 11
2322nfcri 2585 . . . . . . . . . 10
24 mpt2bi123f.8 . . . . . . . . . . 11
2524nfcri 2585 . . . . . . . . . 10
2623, 25nfbi 2016 . . . . . . . . 9
2726nfal 2029 . . . . . . . 8
2827nfal 2029 . . . . . . 7
2928nfri 1951 . . . . . 6
3019, 21, 293syl 18 . . . . 5
31 id 22 . . . . . . . 8
3231alanimi 1687 . . . . . . 7
3332alanimi 1687 . . . . . 6
3433alanimi 1687 . . . . 5
3514, 30, 34syl2an 480 . . . 4
36 eqeq2 2461 . . . . . . . 8
3736alrimiv 1772 . . . . . . 7
3837ralimi 2780 . . . . . 6
3938ralimi 2780 . . . . 5
40 hbra1 2769 . . . . . . . . 9
41 rsp 2753 . . . . . . . . 9
4240, 41alrimih 1692 . . . . . . . 8
43 19.21v 1785 . . . . . . . . 9
4443albii 1690 . . . . . . . 8
4542, 44sylibr 216 . . . . . . 7
4645ralimi 2780 . . . . . 6
47 hbra1 2769 . . . . . . 7
48 rsp 2753 . . . . . . 7
4947, 48alrimih 1692 . . . . . 6
50719.21 1986 . . . . . . . . 9
5150albii 1690 . . . . . . . 8
5251biimpri 210 . . . . . . 7
53 19.21v 1785 . . . . . . . 8
54532albii 1691 . . . . . . 7
5552, 54sylibr 216 . . . . . 6
5646, 49, 553syl 18 . . . . 5
5739, 56syl 17 . . . 4
58 id 22 . . . . . . 7
5958alanimi 1687 . . . . . 6
6059alanimi 1687 . . . . 5
6160alanimi 1687 . . . 4
6235, 57, 61syl2an 480 . . 3
63 tsan2 32377 . . . . . . . . . . . . 13
6463ord 379 . . . . . . . . . . . 12
65 tsan2 32377 . . . . . . . . . . . . 13
6665a1d 26 . . . . . . . . . . . 12
6764, 66cnf1dd 32319 . . . . . . . . . . 11
68 tsbi2 32369 . . . . . . . . . . . . . . 15
6968ord 379 . . . . . . . . . . . . . 14
7069a1dd 47 . . . . . . . . . . . . 13
71 ax-1 6 . . . . . . . . . . . . 13
7270, 71contrd 32326 . . . . . . . . . . . 12
7372a1d 26 . . . . . . . . . . 11
7467, 73cnf1dd 32319 . . . . . . . . . 10
75 idd 25 . . . . . . . . . . . . 13
76 tsan2 32377 . . . . . . . . . . . . . . . . . . 19
7776ord 379 . . . . . . . . . . . . . . . . . 18
78 tsan2 32377 . . . . . . . . . . . . . . . . . . 19
7978a1d 26 . . . . . . . . . . . . . . . . . 18
8077, 79cnf1dd 32319 . . . . . . . . . . . . . . . . 17
81 tsim2 32366 . . . . . . . . . . . . . . . . . 18
8281a1d 26 . . . . . . . . . . . . . . . . 17
8380, 82cnf1dd 32319 . . . . . . . . . . . . . . . 16
84 ax-1 6 . . . . . . . . . . . . . . . 16
8583, 84contrd 32326 . . . . . . . . . . . . . . 15
8685a1d 26 . . . . . . . . . . . . . 14
87 tsbi3 32370 . . . . . . . . . . . . . . 15
8887a1d 26 . . . . . . . . . . . . . 14
8986, 88cnfn2dd 32322 . . . . . . . . . . . . 13
9075, 89cnf1dd 32319 . . . . . . . . . . . 12
91 tsan2 32377 . . . . . . . . . . . . 13
9291a1d 26 . . . . . . . . . . . 12
9390, 92cnf1dd 32319 . . . . . . . . . . 11
94 tsan2 32377 . . . . . . . . . . . 12
9594a1d 26 . . . . . . . . . . 11
9693, 95cnf1dd 32319 . . . . . . . . . 10
9774, 96contrd 32326 . . . . . . . . 9
9897a1d 26 . . . . . . . 8
99 ax-1 6 . . . . . . . . . 10
10081a1d 26 . . . . . . . . . 10
10199, 100cnf2dd 32320 . . . . . . . . 9
102 tsan3 32378 . . . . . . . . . 10
103102a1d 26 . . . . . . . . 9
104101, 103cnfn2dd 32322 . . . . . . . 8
10598, 104mpdd 41 . . . . . . 7
106 notnot2 116 . . . . . . . . . . . . . . . . . 18
107106a1i 11 . . . . . . . . . . . . . . . . 17
10894a1d 26 . . . . . . . . . . . . . . . . 17
109107, 108cnfn2dd 32322 . . . . . . . . . . . . . . . 16
110 tsan3 32378 . . . . . . . . . . . . . . . . 17
111110a1d 26 . . . . . . . . . . . . . . . 16
112109, 111cnfn2dd 32322 . . . . . . . . . . . . . . 15
113 tsan3 32378 . . . . . . . . . . . . . . . . . . 19
114113ord 379 . . . . . . . . . . . . . . . . . 18
11578a1d 26 . . . . . . . . . . . . . . . . . 18
116114, 115cnf1dd 32319 . . . . . . . . . . . . . . . . 17
11781a1d 26 . . . . . . . . . . . . . . . . 17
118116, 117cnf1dd 32319 . . . . . . . . . . . . . . . 16
119 ax-1 6 . . . . . . . . . . . . . . . 16
120118, 119contrd 32326 . . . . . . . . . . . . . . 15
121112, 120sylibrd 238 . . . . . . . . . . . . . 14
12297a1d 26 . . . . . . . . . . . . . . 15
123 ax-1 6 . . . . . . . . . . . . . . . . 17
12481a1d 26 . . . . . . . . . . . . . . . . 17
125123, 124cnf2dd 32320 . . . . . . . . . . . . . . . 16
126102a1d 26 . . . . . . . . . . . . . . . 16
127125, 126cnfn2dd 32322 . . . . . . . . . . . . . . 15
128122, 127mpdd 41 . . . . . . . . . . . . . 14
129121, 128mpdd 41 . . . . . . . . . . . . 13
130122, 121jcad 536 . . . . . . . . . . . . . . 15
131 tsim3 32367 . . . . . . . . . . . . . . . . . . . 20
132131a1d 26 . . . . . . . . . . . . . . . . . . 19
133123, 132cnf2dd 32320 . . . . . . . . . . . . . . . . . 18
134 tsbi1 32368 . . . . . . . . . . . . . . . . . . 19
135134a1d 26 . . . . . . . . . . . . . . . . . 18
136133, 135cnf2dd 32320 . . . . . . . . . . . . . . . . 17
137107, 136cnfn2dd 32322 . . . . . . . . . . . . . . . 16
138 tsan1 32376 . . . . . . . . . . . . . . . . 17
139138a1d 26 . . . . . . . . . . . . . . . 16
140137, 139cnf2dd 32320 . . . . . . . . . . . . . . 15
141130, 140cnfn1dd 32321 . . . . . . . . . . . . . 14
142 tsan3 32378 . . . . . . . . . . . . . . . . 17
143142a1d 26 . . . . . . . . . . . . . . . 16
144107, 143cnfn2dd 32322 . . . . . . . . . . . . . . 15
145 tsbi3 32370 . . . . . . . . . . . . . . . . 17
146145a1d 26 . . . . . . . . . . . . . . . 16
147146or32dd 32323 . . . . . . . . . . . . . . 15
148144, 147cnfn2dd 32322 . . . . . . . . . . . . . 14
149141, 148cnf1dd 32319 . . . . . . . . . . . . 13
150129, 149contrd 32326 . . . . . . . . . . . 12
151150a1d 26 . . . . . . . . . . 11
152131a1d 26 . . . . . . . . . . . . 13
15399, 152cnf2dd 32320 . . . . . . . . . . . 12
15468a1d 26 . . . . . . . . . . . 12
155153, 154cnf2dd 32320 . . . . . . . . . . 11
156151, 155cnf2dd 32320 . . . . . . . . . 10
15765a1d 26 . . . . . . . . . 10
158156, 157cnfn2dd 32322 . . . . . . . . 9
159 tsan3 32378 . . . . . . . . . 10
160159a1d 26 . . . . . . . . 9
161158, 160cnfn2dd 32322 . . . . . . . 8
162 tsan3 32378 . . . . . . . . . . . 12
163162a1d 26 . . . . . . . . . . 11
164156, 163cnfn2dd 32322 . . . . . . . . . 10
16598, 85sylibd 218 . . . . . . . . . . . . 13
166161, 120sylibd 218 . . . . . . . . . . . . 13
167165, 166jcad 536 . . . . . . . . . . . 12
168 tsan1 32376 . . . . . . . . . . . . . 14
169168a1d 26 . . . . . . . . . . . . 13
170151, 169cnf2dd 32320 . . . . . . . . . . . 12
171167, 170cnfn1dd 32321 . . . . . . . . . . 11
172 tsbi4 32371 . . . . . . . . . . . . 13
173172a1d 26 . . . . . . . . . . . 12
174173or32dd 32323 . . . . . . . . . . 11
175171, 174