Metamath Proof Explorer


Theorem infxpenc2lem2

Description: Lemma for infxpenc2 . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Hypotheses infxpenc2.1 φ A On
infxpenc2.2 φ b A ω b w On 1 𝑜 n b : b 1-1 onto ω 𝑜 w
infxpenc2.3 W = x On 1 𝑜 ω 𝑜 x -1 ran n b
infxpenc2.4 φ F : ω 𝑜 2 𝑜 1-1 onto ω
infxpenc2.5 φ F =
infxpenc2.k K = y x ω 𝑜 2 𝑜 W | finSupp x F y I W -1
infxpenc2.h H = ω CNF W K ω 𝑜 2 𝑜 CNF W -1
infxpenc2.l L = y x ω W 𝑜 2 𝑜 | finSupp x I ω y Y X -1 -1
infxpenc2.x X = z 2 𝑜 , w W W 𝑜 z + 𝑜 w
infxpenc2.y Y = z 2 𝑜 , w W 2 𝑜 𝑜 w + 𝑜 z
infxpenc2.j J = ω CNF 2 𝑜 𝑜 W L ω CNF W 𝑜 2 𝑜 -1
infxpenc2.z Z = x ω 𝑜 W , y ω 𝑜 W ω 𝑜 W 𝑜 x + 𝑜 y
infxpenc2.t T = x b , y b n b x n b y
infxpenc2.g G = n b -1 H J Z T
Assertion infxpenc2lem2 φ g b A ω b g b : b × b 1-1 onto b

Proof

Step Hyp Ref Expression
1 infxpenc2.1 φ A On
2 infxpenc2.2 φ b A ω b w On 1 𝑜 n b : b 1-1 onto ω 𝑜 w
3 infxpenc2.3 W = x On 1 𝑜 ω 𝑜 x -1 ran n b
4 infxpenc2.4 φ F : ω 𝑜 2 𝑜 1-1 onto ω
5 infxpenc2.5 φ F =
6 infxpenc2.k K = y x ω 𝑜 2 𝑜 W | finSupp x F y I W -1
7 infxpenc2.h H = ω CNF W K ω 𝑜 2 𝑜 CNF W -1
8 infxpenc2.l L = y x ω W 𝑜 2 𝑜 | finSupp x I ω y Y X -1 -1
9 infxpenc2.x X = z 2 𝑜 , w W W 𝑜 z + 𝑜 w
10 infxpenc2.y Y = z 2 𝑜 , w W 2 𝑜 𝑜 w + 𝑜 z
11 infxpenc2.j J = ω CNF 2 𝑜 𝑜 W L ω CNF W 𝑜 2 𝑜 -1
12 infxpenc2.z Z = x ω 𝑜 W , y ω 𝑜 W ω 𝑜 W 𝑜 x + 𝑜 y
13 infxpenc2.t T = x b , y b n b x n b y
14 infxpenc2.g G = n b -1 H J Z T
15 1 mptexd φ b A G V
16 1 adantr φ b A ω b A On
17 simprl φ b A ω b b A
18 onelon A On b A b On
19 16 17 18 syl2anc φ b A ω b b On
20 simprr φ b A ω b ω b
21 1 2 3 infxpenc2lem1 φ b A ω b W On 1 𝑜 n b : b 1-1 onto ω 𝑜 W
22 21 simpld φ b A ω b W On 1 𝑜
23 4 adantr φ b A ω b F : ω 𝑜 2 𝑜 1-1 onto ω
24 5 adantr φ b A ω b F =
25 21 simprd φ b A ω b n b : b 1-1 onto ω 𝑜 W
26 19 20 22 23 24 25 6 7 8 9 10 11 12 13 14 infxpenc φ b A ω b G : b × b 1-1 onto b
27 f1of G : b × b 1-1 onto b G : b × b b
28 26 27 syl φ b A ω b G : b × b b
29 vex b V
30 29 29 xpex b × b V
31 fex G : b × b b b × b V G V
32 28 30 31 sylancl φ b A ω b G V
33 eqid b A G = b A G
34 33 fvmpt2 b A G V b A G b = G
35 17 32 34 syl2anc φ b A ω b b A G b = G
36 35 f1oeq1d φ b A ω b b A G b : b × b 1-1 onto b G : b × b 1-1 onto b
37 26 36 mpbird φ b A ω b b A G b : b × b 1-1 onto b
38 37 expr φ b A ω b b A G b : b × b 1-1 onto b
39 38 ralrimiva φ b A ω b b A G b : b × b 1-1 onto b
40 nfmpt1 _ b b A G
41 40 nfeq2 b g = b A G
42 fveq1 g = b A G g b = b A G b
43 42 f1oeq1d g = b A G g b : b × b 1-1 onto b b A G b : b × b 1-1 onto b
44 43 imbi2d g = b A G ω b g b : b × b 1-1 onto b ω b b A G b : b × b 1-1 onto b
45 41 44 ralbid g = b A G b A ω b g b : b × b 1-1 onto b b A ω b b A G b : b × b 1-1 onto b
46 15 39 45 spcedv φ g b A ω b g b : b × b 1-1 onto b