Metamath Proof Explorer


Theorem axcc2lem

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

Ref Expression
Hypotheses axcc2lem.1 K = n ω if F n = F n
axcc2lem.2 A = n ω n × K n
axcc2lem.3 G = n ω 2 nd f A n
Assertion axcc2lem g g Fn ω n ω F n g n F n

Proof

Step Hyp Ref Expression
1 axcc2lem.1 K = n ω if F n = F n
2 axcc2lem.2 A = n ω n × K n
3 axcc2lem.3 G = n ω 2 nd f A n
4 fvex 2 nd f A n V
5 4 3 fnmpti G Fn ω
6 snex n V
7 fvex K n V
8 6 7 xpex n × K n V
9 2 fvmpt2 n ω n × K n V A n = n × K n
10 8 9 mpan2 n ω A n = n × K n
11 vex n V
12 11 snnz n
13 0ex V
14 13 snnz
15 iftrue F n = if F n = F n =
16 15 neeq1d F n = if F n = F n
17 14 16 mpbiri F n = if F n = F n
18 iffalse ¬ F n = if F n = F n = F n
19 neqne ¬ F n = F n
20 18 19 eqnetrd ¬ F n = if F n = F n
21 17 20 pm2.61i if F n = F n
22 p0ex V
23 fvex F n V
24 22 23 ifex if F n = F n V
25 1 fvmpt2 n ω if F n = F n V K n = if F n = F n
26 24 25 mpan2 n ω K n = if F n = F n
27 26 neeq1d n ω K n if F n = F n
28 21 27 mpbiri n ω K n
29 xpnz n K n n × K n
30 29 biimpi n K n n × K n
31 12 28 30 sylancr n ω n × K n
32 10 31 eqnetrd n ω A n
33 8 2 fnmpti A Fn ω
34 fnfvelrn A Fn ω n ω A n ran A
35 33 34 mpan n ω A n ran A
36 neeq1 z = A n z A n
37 fveq2 z = A n f z = f A n
38 id z = A n z = A n
39 37 38 eleq12d z = A n f z z f A n A n
40 36 39 imbi12d z = A n z f z z A n f A n A n
41 40 rspccv z ran A z f z z A n ran A A n f A n A n
42 35 41 syl5 z ran A z f z z n ω A n f A n A n
43 32 42 mpdi z ran A z f z z n ω f A n A n
44 43 impcom n ω z ran A z f z z f A n A n
45 10 eleq2d n ω f A n A n f A n n × K n
46 45 adantr n ω z ran A z f z z f A n A n f A n n × K n
47 44 46 mpbid n ω z ran A z f z z f A n n × K n
48 xp2nd f A n n × K n 2 nd f A n K n
49 47 48 syl n ω z ran A z f z z 2 nd f A n K n
50 49 3adant3 n ω z ran A z f z z F n 2 nd f A n K n
51 3 fvmpt2 n ω 2 nd f A n V G n = 2 nd f A n
52 4 51 mpan2 n ω G n = 2 nd f A n
53 52 3ad2ant1 n ω z ran A z f z z F n G n = 2 nd f A n
54 53 eqcomd n ω z ran A z f z z F n 2 nd f A n = G n
55 26 3ad2ant1 n ω z ran A z f z z F n K n = if F n = F n
56 ifnefalse F n if F n = F n = F n
57 56 3ad2ant3 n ω z ran A z f z z F n if F n = F n = F n
58 55 57 eqtrd n ω z ran A z f z z F n K n = F n
59 50 54 58 3eltr3d n ω z ran A z f z z F n G n F n
60 59 3expia n ω z ran A z f z z F n G n F n
61 60 expcom z ran A z f z z n ω F n G n F n
62 61 ralrimiv z ran A z f z z n ω F n G n F n
63 omex ω V
64 fnex G Fn ω ω V G V
65 5 63 64 mp2an G V
66 fneq1 g = G g Fn ω G Fn ω
67 fveq1 g = G g n = G n
68 67 eleq1d g = G g n F n G n F n
69 68 imbi2d g = G F n g n F n F n G n F n
70 69 ralbidv g = G n ω F n g n F n n ω F n G n F n
71 66 70 anbi12d g = G g Fn ω n ω F n g n F n G Fn ω n ω F n G n F n
72 65 71 spcev G Fn ω n ω F n G n F n g g Fn ω n ω F n g n F n
73 5 62 72 sylancr z ran A z f z z g g Fn ω n ω F n g n F n
74 8 a1i ω V n ω n × K n V
75 74 2 fmptd ω V A : ω V
76 63 75 ax-mp A : ω V
77 sneq n = k n = k
78 fveq2 n = k K n = K k
79 77 78 xpeq12d n = k n × K n = k × K k
80 79 2 8 fvmpt3i k ω A k = k × K k
81 80 adantl n ω k ω A k = k × K k
82 81 eqeq2d n ω k ω A n = A k A n = k × K k
83 10 adantr n ω k ω A n = n × K n
84 83 eqeq1d n ω k ω A n = k × K k n × K n = k × K k
85 xp11 n K n n × K n = k × K k n = k K n = K k
86 12 28 85 sylancr n ω n × K n = k × K k n = k K n = K k
87 11 sneqr n = k n = k
88 87 adantr n = k K n = K k n = k
89 86 88 syl6bi n ω n × K n = k × K k n = k
90 89 adantr n ω k ω n × K n = k × K k n = k
91 84 90 sylbid n ω k ω A n = k × K k n = k
92 82 91 sylbid n ω k ω A n = A k n = k
93 92 rgen2 n ω k ω A n = A k n = k
94 dff13 A : ω 1-1 V A : ω V n ω k ω A n = A k n = k
95 76 93 94 mpbir2an A : ω 1-1 V
96 f1f1orn A : ω 1-1 V A : ω 1-1 onto ran A
97 63 f1oen A : ω 1-1 onto ran A ω ran A
98 ensym ω ran A ran A ω
99 96 97 98 3syl A : ω 1-1 V ran A ω
100 2 rneqi ran A = ran n ω n × K n
101 dmmptg n ω n × K n V dom n ω n × K n = ω
102 8 a1i n ω n × K n V
103 101 102 mprg dom n ω n × K n = ω
104 103 63 eqeltri dom n ω n × K n V
105 funmpt Fun n ω n × K n
106 funrnex dom n ω n × K n V Fun n ω n × K n ran n ω n × K n V
107 104 105 106 mp2 ran n ω n × K n V
108 100 107 eqeltri ran A V
109 breq1 a = ran A a ω ran A ω
110 raleq a = ran A z a z f z z z ran A z f z z
111 110 exbidv a = ran A f z a z f z z f z ran A z f z z
112 109 111 imbi12d a = ran A a ω f z a z f z z ran A ω f z ran A z f z z
113 ax-cc a ω f z a z f z z
114 108 112 113 vtocl ran A ω f z ran A z f z z
115 95 99 114 mp2b f z ran A z f z z
116 73 115 exlimiiv g g Fn ω n ω F n g n F n