NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  xpassen Unicode version

Theorem xpassen 6057
Description: Associative law for equinumerosity of cross product. Proposition 4.22(e) of [Mendelson] p. 254. (Contributed by SF, 24-Feb-2015.)
Hypotheses
Ref Expression
xpassen.1
xpassen.2
xpassen.3
Assertion
Ref Expression
xpassen

Proof of Theorem xpassen
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1stfo 5505 . . . . . . . . . . 11
2 fof 5269 . . . . . . . . . . 11
31, 2ax-mp 5 . . . . . . . . . 10
4 dffn2 5224 . . . . . . . . . 10
53, 4mpbir 200 . . . . . . . . 9
6 ssv 3291 . . . . . . . . 9
7 fnco 5191 . . . . . . . . 9
85, 5, 6, 7mp3an 1277 . . . . . . . 8
9 2ndfo 5506 . . . . . . . . . . . 12
10 fofn 5271 . . . . . . . . . . . 12
119, 10ax-mp 5 . . . . . . . . . . 11
12 fnco 5191 . . . . . . . . . . 11
1311, 5, 6, 12mp3an 1277 . . . . . . . . . 10
14 fntxp 5804 . . . . . . . . . 10
1513, 11, 14mp2an 653 . . . . . . . . 9
16 inidm 3464 . . . . . . . . . 10
1716fneq2i 5179 . . . . . . . . 9
1815, 17mpbi 199 . . . . . . . 8
19 fntxp 5804 . . . . . . . 8
208, 18, 19mp2an 653 . . . . . . 7
2116fneq2i 5179 . . . . . . 7
2220, 21mpbi 199 . . . . . 6
23 dffn2 5224 . . . . . 6
2422, 23mpbi 199 . . . . 5
25 xpassenlem 6056 . . . . . . . . 9 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2
26 xpassenlem 6056 . . . . . . . . 9 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2
27 simp1 955 . . . . . . . . . . . . . 14 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1 Proj1
28 simp1 955 . . . . . . . . . . . . . 14 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1 Proj1
29 eqtr3 2372 . . . . . . . . . . . . . 14 Proj1 Proj1 Proj1 Proj1 Proj1 Proj1 Proj1 Proj1 Proj1 Proj1
3027, 28, 29syl2an 463 . . . . . . . . . . . . 13 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1 Proj1 Proj1
31 simp2 956 . . . . . . . . . . . . . 14 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1 Proj2
32 simp2 956 . . . . . . . . . . . . . 14 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1 Proj2
33 eqtr3 2372 . . . . . . . . . . . . . 14 Proj2 Proj1 Proj1 Proj2 Proj2 Proj1 Proj1 Proj2 Proj2 Proj1 Proj2 Proj1
3431, 32, 33syl2an 463 . . . . . . . . . . . . 13 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj2 Proj1 Proj2 Proj1
3530, 34opeq12d 4586 . . . . . . . . . . . 12 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1 Proj2 Proj1 Proj1 Proj1 Proj2 Proj1
36 opeq 4619 . . . . . . . . . . . 12 Proj1 Proj1 Proj1 Proj2 Proj1
37 opeq 4619 . . . . . . . . . . . 12 Proj1 Proj1 Proj1 Proj2 Proj1
3835, 36, 373eqtr4g 2410 . . . . . . . . . . 11 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1
39 simp3 957 . . . . . . . . . . . 12 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj2 Proj2 Proj2
40 simp3 957 . . . . . . . . . . . 12 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj2 Proj2 Proj2
41 eqtr3 2372 . . . . . . . . . . . 12 Proj2 Proj2 Proj2 Proj2 Proj2 Proj2 Proj2 Proj2
4239, 40, 41syl2an 463 . . . . . . . . . . 11 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj2 Proj2
4338, 42opeq12d 4586 . . . . . . . . . 10 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj1 Proj2 Proj1 Proj2
44 opeq 4619 . . . . . . . . . 10 Proj1 Proj2
45 opeq 4619 . . . . . . . . . 10 Proj1 Proj2
4643, 44, 453eqtr4g 2410 . . . . . . . . 9 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2 Proj1 Proj1 Proj1 Proj2 Proj1 Proj1 Proj2 Proj2 Proj2 Proj2
4725, 26, 46syl2anb 465 . . . . . . . 8
4847gen2 1547 . . . . . . 7
49 breq1 4642 . . . . . . . 8
5049mo4 2237 . . . . . . 7
5148, 50mpbir 200 . . . . . 6
5251ax-gen 1546 . . . . 5
53 dff12 5257 . . . . 5
5424, 52, 53mpbir2an 886 . . . 4
55 ssv 3291 . . . 4
56 f1ores 5300 . . . 4
5754, 55, 56mp2an 653 . . 3
58 vex 2862 . . . . . 6
59 opeqex 4621 . . . . . 6
60 rexcom4 2878 . . . . . . . . . . . 12
61 rexcom4 2878 . . . . . . . . . . . . . 14
62 rexcom4 2878 . . . . . . . . . . . . . . . 16
63 vex 2862 . . . . . . . . . . . . . . . . . . . . 21
64 vex 2862 . . . . . . . . . . . . . . . . . . . . 21
6563, 64opex 4588 . . . . . . . . . . . . . . . . . . . 20
66 vex 2862 . . . . . . . . . . . . . . . . . . . 20
6765, 66opex 4588 . . . . . . . . . . . . . . . . . . 19
68 breq1 4642 . . . . . . . . . . . . . . . . . . 19
6967, 68ceqsexv 2894 . . . . . . . . . . . . . . . . . 18
7065, 66brco1st 5777 . . . . . . . . . . . . . . . . . . . . 21
7163, 64opbr1st 5501 . . . . . . . . . . . . . . . . . . . . 21
7270, 71bitri 240 . . . . . . . . . . . . . . . . . . . 20
73 trtxp 5781 . . . . . . . . . . . . . . . . . . . . 21
74 brco 4883 . . . . . . . . . . . . . . . . . . . . . . 23
7565, 66opbr1st 5501 . . . . . . . . . . . . . . . . . . . . . . . . . 26
76 eqcom 2355 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7775, 76bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25
7877anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . 24
7978exbii 1582 . . . . . . . . . . . . . . . . . . . . . . 23
80 breq1 4642 . . . . . . . . . . . . . . . . . . . . . . . . 25
8165, 80ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . 24
8263, 64opbr2nd 5502 . . . . . . . . . . . . . . . . . . . . . . . 24
8381, 82bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23
8474, 79, 833bitri 262 . . . . . . . . . . . . . . . . . . . . . 22
8565, 66opbr2nd 5502 . . . . . . . . . . . . . . . . . . . . . 22
8684, 85anbi12i 678 . . . . . . . . . . . . . . . . . . . . 21
8773, 86bitri 240 . . . . . . . . . . . . . . . . . . . 20
8872, 87anbi12i 678 . . . . . . . . . . . . . . . . . . 19
89 trtxp 5781 . . . . . . . . . . . . . . . . . . 19
90 3anass 938 . . . . . . . . . . . . . . . . . . 19
9188, 89, 903bitr4i 268 . . . . . . . . . . . . . . . . . 18
9269, 91bitri 240 . . . . . . . . . . . . . . . . 17
9392rexbii 2639 . . . . . . . . . . . . . . . 16
9462, 93bitr3i 242 . . . . . . . . . . . . . . 15
9594rexbii 2639 . . . . . . . . . . . . . 14
9661, 95bitr3i 242 . . . . . . . . . . . . 13
9796rexbii 2639 . . . . . . . . . . . 12
9860, 97bitr3i 242 . . . . . . . . . . 11
99 3reeanv 2779 . . . . . . . . . . 11
10098, 99bitri 240 . . . . . . . . . 10
101 r19.41v 2764 . . . . . . . . . . . 12
102 r19.41v 2764 . . . . . . . . . . . . . . 15
103102rexbii 2639 . . . . . . . . . . . . . 14
104 r19.41v 2764 . . . . . . . . . . . . . 14
105103, 104bitri 240 . . . . . . . . . . . . 13
106105rexbii 2639 . . . . . . . . . . . 12
107 elxp2 4802 . . . . . . . . . . . . . 14
108 df-rex 2620 . . . . . . . . . . . . . 14
109 rexcom4 2878 . . . . . . . . . . . . . . 15
110 opeq1 4578 . . . . . . . . . . . . . . . . . . . . . 22
111110eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21
11265, 111ceqsexv 2894 . . . . . . . . . . . . . . . . . . . 20
113112rexbii 2639 . . . . . . . . . . . . . . . . . . 19
114 rexcom4 2878 . . . . . . . . . . . . . . . . . . 19
115113, 114bitr3i 242 . . . . . . . . . . . . . . . . . 18
116115rexbii 2639 . . . . . . . . . . . . . . . . 17
117 rexcom4 2878 . . . . . . . . . . . . . . . . 17
118116, 117bitri 240 . . . . . . . . . . . . . . . 16
119118rexbii 2639 . . . . . . . . . . . . . . 15
120 r19.41v 2764 . . . . . . . . . . . . . . . . 17
121 reeanv 2778 . . . . . . . . . . . . . . . . . 18
122121rexbii 2639 . . . . . . . . . . . . . . . . 17
123 elxp2 4802 . . . . . . . . . . . . . . . . . 18
124123anbi1i 676 . . . . . . . . . . . . . . . . 17
125120, 122, 1243bitr4ri 269 . . . . . . . . . . . . . . . 16
126125exbii 1582 . . . . . . . . . . . . . . 15
127109, 119, 1263bitr4ri 269 . . . . . . . . . . . . . 14
128107, 108, 1273bitri 262 . . . . . . . . . . . . 13
129128anbi1i 676 . . . . . . . . . . . 12
130101, 106, 1293bitr4ri 269 . . . . . . . . . . 11
131130exbii 1582 . . . . . . . . . 10
132 risset 2661 . . . . . . . . . . 11
133 risset 2661 . . . . . . . . . . 11
134 risset 2661 . . . . . . . . . . 11
135132, 133, 1343anbi123i 1140 . . . . . . . . . 10
136100, 131, 1353bitr4i 268 . . . . . . . . 9
137 elima2 4755 . . . . . . . . 9
138 opelxp 4811 . . . . . . . . . . 11
139138anbi2i 675 . . . . . . . . . 10
140 opelxp 4811 . . . . . . . . . 10
141 3anass 938 . . . . . . . . . 10
142139, 140, 1413bitr4i 268 . . . . . . . . 9
143136, 137, 1423bitr4i 268 . . . . . . . 8
144 opeq2 4579 . . . . . . . . . 10
145144eleq1d 2419 . . . . . . . . 9
146144eleq1d 2419 . . . . . . . . 9
147145, 146bibi12d 312 . . . . . . . 8
148143, 147mpbiri 224 . . . . . . 7
149148exlimivv 1635 . . . . . 6
15058, 59, 149mp2b 9 . . . . 5
151150eqrelriv 4850 . . . 4
152 f1oeq3 5283 . . . 4
153151, 152ax-mp 5 . . 3
15457, 153mpbi 199 . 2
155 1stex 4739 . . . . . 6
156155, 155coex 4750 . . . . 5
157 2ndex 5112 . . . . . . 7
158157, 155coex 4750 . . . . . 6
159158, 157txpex 5785 . . . . 5
160156, 159txpex 5785 . . . 4
161 xpassen.1 . . . . . 6
162 xpassen.2 . . . . . 6
163161, 162xpex 5115 . . . . 5
164 xpassen.3 . . . . 5
165163, 164xpex 5115 . . . 4
166160, 165resex 5117 . . 3
167166f1oen 6033 . 2
168154, 167ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176   wa 358   w3a 934  wal 1540  wex 1541   wceq 1642   wcel 1710  wmo 2205  wrex 2615  cvv 2859   cin 3208   wss 3257  cop 4561   Proj1 cproj1 4563   Proj2 cproj2 4564   class class class wbr 4639  c1st 4717   ccom 4721  cima 4722   cxp 4770   crn 4773   cres 4774   wfn 4776  wf 4777  wf1 4778  wfo 4779  wf1o 4780  c2nd 4783   ctxp 5735   cen 6028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-co 4726  df-ima 4727  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-dm 4787  df-res 4788  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-2nd 4797  df-txp 5736  df-en 6029
This theorem is referenced by:  mucass  6135
  Copyright terms: Public domain W3C validator