Metamath Proof Explorer


Theorem cantnflem4

Description: Lemma for cantnf . Complete the induction step of cantnflem3 . (Contributed by Mario Carneiro, 25-May-2015)

Ref Expression
Hypotheses cantnfs.s S=domACNFB
cantnfs.a φAOn
cantnfs.b φBOn
oemapval.t T=xy|zBxzyzwBzwxw=yw
cantnf.c φCA𝑜B
cantnf.s φCranACNFB
cantnf.e φC
cantnf.x X=cOn|CA𝑜c
cantnf.p P=ιd|aOnbA𝑜Xd=abA𝑜X𝑜a+𝑜b=C
cantnf.y Y=1stP
cantnf.z Z=2ndP
Assertion cantnflem4 φCranACNFB

Proof

Step Hyp Ref Expression
1 cantnfs.s S=domACNFB
2 cantnfs.a φAOn
3 cantnfs.b φBOn
4 oemapval.t T=xy|zBxzyzwBzwxw=yw
5 cantnf.c φCA𝑜B
6 cantnf.s φCranACNFB
7 cantnf.e φC
8 cantnf.x X=cOn|CA𝑜c
9 cantnf.p P=ιd|aOnbA𝑜Xd=abA𝑜X𝑜a+𝑜b=C
10 cantnf.y Y=1stP
11 cantnf.z Z=2ndP
12 1 2 3 4 5 6 7 cantnflem2 φAOn2𝑜COn1𝑜
13 eqid X=X
14 eqid Y=Y
15 eqid Z=Z
16 13 14 15 3pm3.2i X=XY=YZ=Z
17 8 9 10 11 oeeui AOn2𝑜COn1𝑜XOnYA1𝑜ZA𝑜XA𝑜X𝑜Y+𝑜Z=CX=XY=YZ=Z
18 16 17 mpbiri AOn2𝑜COn1𝑜XOnYA1𝑜ZA𝑜XA𝑜X𝑜Y+𝑜Z=C
19 12 18 syl φXOnYA1𝑜ZA𝑜XA𝑜X𝑜Y+𝑜Z=C
20 19 simpld φXOnYA1𝑜ZA𝑜X
21 20 simp1d φXOn
22 oecl AOnXOnA𝑜XOn
23 2 21 22 syl2anc φA𝑜XOn
24 20 simp2d φYA1𝑜
25 24 eldifad φYA
26 onelon AOnYAYOn
27 2 25 26 syl2anc φYOn
28 omcl A𝑜XOnYOnA𝑜X𝑜YOn
29 23 27 28 syl2anc φA𝑜X𝑜YOn
30 20 simp3d φZA𝑜X
31 onelon A𝑜XOnZA𝑜XZOn
32 23 30 31 syl2anc φZOn
33 oaword1 A𝑜X𝑜YOnZOnA𝑜X𝑜YA𝑜X𝑜Y+𝑜Z
34 29 32 33 syl2anc φA𝑜X𝑜YA𝑜X𝑜Y+𝑜Z
35 dif1o YA1𝑜YAY
36 35 simprbi YA1𝑜Y
37 24 36 syl φY
38 on0eln0 YOnYY
39 27 38 syl φYY
40 37 39 mpbird φY
41 omword1 A𝑜XOnYOnYA𝑜XA𝑜X𝑜Y
42 23 27 40 41 syl21anc φA𝑜XA𝑜X𝑜Y
43 42 30 sseldd φZA𝑜X𝑜Y
44 34 43 sseldd φZA𝑜X𝑜Y+𝑜Z
45 19 simprd φA𝑜X𝑜Y+𝑜Z=C
46 44 45 eleqtrd φZC
47 6 46 sseldd φZranACNFB
48 1 2 3 cantnff φACNFB:SA𝑜B
49 ffn ACNFB:SA𝑜BACNFBFnS
50 fvelrnb ACNFBFnSZranACNFBgSACNFBg=Z
51 48 49 50 3syl φZranACNFBgSACNFBg=Z
52 47 51 mpbid φgSACNFBg=Z
53 2 adantr φgSACNFBg=ZAOn
54 3 adantr φgSACNFBg=ZBOn
55 5 adantr φgSACNFBg=ZCA𝑜B
56 6 adantr φgSACNFBg=ZCranACNFB
57 7 adantr φgSACNFBg=ZC
58 simprl φgSACNFBg=ZgS
59 simprr φgSACNFBg=ZACNFBg=Z
60 eqid tBift=XYgt=tBift=XYgt
61 1 53 54 4 55 56 57 8 9 10 11 58 59 60 cantnflem3 φgSACNFBg=ZCranACNFB
62 52 61 rexlimddv φCranACNFB