Metamath Proof Explorer


Theorem axcc2lem

Description: Lemma for axcc2 . (Contributed by Mario Carneiro, 8-Feb-2013)

Ref Expression
Hypotheses axcc2lem.1 K=nωifFn=Fn
axcc2lem.2 A=nωn×Kn
axcc2lem.3 G=nω2ndfAn
Assertion axcc2lem ggFnωnωFngnFn

Proof

Step Hyp Ref Expression
1 axcc2lem.1 K=nωifFn=Fn
2 axcc2lem.2 A=nωn×Kn
3 axcc2lem.3 G=nω2ndfAn
4 fvex 2ndfAnV
5 4 3 fnmpti GFnω
6 snex nV
7 fvex KnV
8 6 7 xpex n×KnV
9 2 fvmpt2 nωn×KnVAn=n×Kn
10 8 9 mpan2 nωAn=n×Kn
11 vex nV
12 11 snnz n
13 0ex V
14 13 snnz
15 iftrue Fn=ifFn=Fn=
16 15 neeq1d Fn=ifFn=Fn
17 14 16 mpbiri Fn=ifFn=Fn
18 iffalse ¬Fn=ifFn=Fn=Fn
19 neqne ¬Fn=Fn
20 18 19 eqnetrd ¬Fn=ifFn=Fn
21 17 20 pm2.61i ifFn=Fn
22 p0ex V
23 fvex FnV
24 22 23 ifex ifFn=FnV
25 1 fvmpt2 nωifFn=FnVKn=ifFn=Fn
26 24 25 mpan2 nωKn=ifFn=Fn
27 26 neeq1d nωKnifFn=Fn
28 21 27 mpbiri nωKn
29 xpnz nKnn×Kn
30 29 biimpi nKnn×Kn
31 12 28 30 sylancr nωn×Kn
32 10 31 eqnetrd nωAn
33 8 2 fnmpti AFnω
34 fnfvelrn AFnωnωAnranA
35 33 34 mpan nωAnranA
36 neeq1 z=AnzAn
37 fveq2 z=Anfz=fAn
38 id z=Anz=An
39 37 38 eleq12d z=AnfzzfAnAn
40 36 39 imbi12d z=AnzfzzAnfAnAn
41 40 rspccv zranAzfzzAnranAAnfAnAn
42 35 41 syl5 zranAzfzznωAnfAnAn
43 32 42 mpdi zranAzfzznωfAnAn
44 43 impcom nωzranAzfzzfAnAn
45 10 eleq2d nωfAnAnfAnn×Kn
46 45 adantr nωzranAzfzzfAnAnfAnn×Kn
47 44 46 mpbid nωzranAzfzzfAnn×Kn
48 xp2nd fAnn×Kn2ndfAnKn
49 47 48 syl nωzranAzfzz2ndfAnKn
50 49 3adant3 nωzranAzfzzFn2ndfAnKn
51 3 fvmpt2 nω2ndfAnVGn=2ndfAn
52 4 51 mpan2 nωGn=2ndfAn
53 52 3ad2ant1 nωzranAzfzzFnGn=2ndfAn
54 53 eqcomd nωzranAzfzzFn2ndfAn=Gn
55 26 3ad2ant1 nωzranAzfzzFnKn=ifFn=Fn
56 ifnefalse FnifFn=Fn=Fn
57 56 3ad2ant3 nωzranAzfzzFnifFn=Fn=Fn
58 55 57 eqtrd nωzranAzfzzFnKn=Fn
59 50 54 58 3eltr3d nωzranAzfzzFnGnFn
60 59 3expia nωzranAzfzzFnGnFn
61 60 expcom zranAzfzznωFnGnFn
62 61 ralrimiv zranAzfzznωFnGnFn
63 omex ωV
64 fnex GFnωωVGV
65 5 63 64 mp2an GV
66 fneq1 g=GgFnωGFnω
67 fveq1 g=Ggn=Gn
68 67 eleq1d g=GgnFnGnFn
69 68 imbi2d g=GFngnFnFnGnFn
70 69 ralbidv g=GnωFngnFnnωFnGnFn
71 66 70 anbi12d g=GgFnωnωFngnFnGFnωnωFnGnFn
72 65 71 spcev GFnωnωFnGnFnggFnωnωFngnFn
73 5 62 72 sylancr zranAzfzzggFnωnωFngnFn
74 8 a1i ωVnωn×KnV
75 74 2 fmptd ωVA:ωV
76 63 75 ax-mp A:ωV
77 sneq n=kn=k
78 fveq2 n=kKn=Kk
79 77 78 xpeq12d n=kn×Kn=k×Kk
80 79 2 8 fvmpt3i kωAk=k×Kk
81 80 adantl nωkωAk=k×Kk
82 81 eqeq2d nωkωAn=AkAn=k×Kk
83 10 adantr nωkωAn=n×Kn
84 83 eqeq1d nωkωAn=k×Kkn×Kn=k×Kk
85 xp11 nKnn×Kn=k×Kkn=kKn=Kk
86 12 28 85 sylancr nωn×Kn=k×Kkn=kKn=Kk
87 11 sneqr n=kn=k
88 87 adantr n=kKn=Kkn=k
89 86 88 syl6bi nωn×Kn=k×Kkn=k
90 89 adantr nωkωn×Kn=k×Kkn=k
91 84 90 sylbid nωkωAn=k×Kkn=k
92 82 91 sylbid nωkωAn=Akn=k
93 92 rgen2 nωkωAn=Akn=k
94 dff13 A:ω1-1VA:ωVnωkωAn=Akn=k
95 76 93 94 mpbir2an A:ω1-1V
96 f1f1orn A:ω1-1VA:ω1-1 ontoranA
97 63 f1oen A:ω1-1 ontoranAωranA
98 ensym ωranAranAω
99 96 97 98 3syl A:ω1-1VranAω
100 2 rneqi ranA=rannωn×Kn
101 dmmptg nωn×KnVdomnωn×Kn=ω
102 8 a1i nωn×KnV
103 101 102 mprg domnωn×Kn=ω
104 103 63 eqeltri domnωn×KnV
105 funmpt Funnωn×Kn
106 funrnex domnωn×KnVFunnωn×Knrannωn×KnV
107 104 105 106 mp2 rannωn×KnV
108 100 107 eqeltri ranAV
109 breq1 a=ranAaωranAω
110 raleq a=ranAzazfzzzranAzfzz
111 110 exbidv a=ranAfzazfzzfzranAzfzz
112 109 111 imbi12d a=ranAaωfzazfzzranAωfzranAzfzz
113 ax-cc aωfzazfzz
114 108 112 113 vtocl ranAωfzranAzfzz
115 95 99 114 mp2b fzranAzfzz
116 73 115 exlimiiv ggFnωnωFngnFn