Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwfseqlem5 Structured version   Unicode version

Theorem pwfseqlem5 8543
 Description: Lemma for pwfseq 8544. Although in some ways pwfseqlem4 8542 is the "main" part of the proof, one last aspect which makes up a remark in the original text is by far the hardest part to formalize. The main proof relies on the existence of an injection from the set of finite sequences on an infinite set to . Now this alone would not be difficult to prove; this is mostly the claim of fseqen 7913. However, what is needed for the proof is a canonical injection on these sets, so we have to start from scratch pulling together explicit bijections from the lemmas. If one attempts such a program, it will mostly go through, but there is one key step which is inherently nonconstructive, namely the proof of infxpen 7901. The resolution is not obvious, but it turns out that reversing an infinite ordinal's Cantor normal form absorbs all the non-leading terms (cnfcom3c 7666), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 7904). (Contributed by Mario Carneiro, 31-May-2015.)
Hypotheses
Ref Expression
pwfseqlem5.g
pwfseqlem5.x
pwfseqlem5.h
pwfseqlem5.ps
pwfseqlem5.n har
pwfseqlem5.o OrdIso
pwfseqlem5.t
pwfseqlem5.p
pwfseqlem5.s seq𝜔
pwfseqlem5.q
pwfseqlem5.i
pwfseqlem5.k
Assertion
Ref Expression
pwfseqlem5
Distinct variable groups:   ,,   ,,,   ,,,   ,,,,,,,,,   ,,,,,,,   ,,   ,   ,,,,   ,,   ,,,,   ,,,,,
Allowed substitution hints:   (,,)   (,,,,,)   (,,,,,)   (,,,,,,)   (,,,,,,,,,)   (,,,,,,,)   (,,,,,,,,,)   (,,,,,,,)   (,,,,,,)   (,,,,,,,,,)   (,,,,,,,)   (,,,,,,,,)   (,,,,)   (,,,,,,,,,)

Proof of Theorem pwfseqlem5
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pwfseqlem5.g . 2
2 pwfseqlem5.x . 2
3 pwfseqlem5.h . 2
4 pwfseqlem5.ps . 2
5 vex 2961 . . . . . . . . . . 11
6 simprl3 1005 . . . . . . . . . . . 12
74, 6sylan2b 463 . . . . . . . . . . 11
8 pwfseqlem5.o . . . . . . . . . . . 12 OrdIso
98oiiso 7509 . . . . . . . . . . 11
105, 7, 9sylancr 646 . . . . . . . . . 10
11 isof1o 6048 . . . . . . . . . 10
1210, 11syl 16 . . . . . . . . 9
138oion 7508 . . . . . . . . . . . . 13
145, 13ax-mp 5 . . . . . . . . . . . 12
1514a1i 11 . . . . . . . . . . 11
168oien 7510 . . . . . . . . . . . . 13
175, 7, 16sylancr 646 . . . . . . . . . . . 12
181adantr 453 . . . . . . . . . . . . . . . 16
19 omex 7601 . . . . . . . . . . . . . . . . 17
20 ovex 6109 . . . . . . . . . . . . . . . . 17
2119, 20iunex 5994 . . . . . . . . . . . . . . . 16
22 f1dmex 5974 . . . . . . . . . . . . . . . 16
2318, 21, 22sylancl 645 . . . . . . . . . . . . . . 15
24 pwexb 4756 . . . . . . . . . . . . . . 15
2523, 24sylibr 205 . . . . . . . . . . . . . 14
26 simprl1 1003 . . . . . . . . . . . . . . 15
274, 26sylan2b 463 . . . . . . . . . . . . . 14
28 ssdomg 7156 . . . . . . . . . . . . . 14
2925, 27, 28sylc 59 . . . . . . . . . . . . 13
30 canth2g 7264 . . . . . . . . . . . . . 14
31 sdomdom 7138 . . . . . . . . . . . . . 14
3225, 30, 313syl 19 . . . . . . . . . . . . 13
33 domtr 7163 . . . . . . . . . . . . 13
3429, 32, 33syl2anc 644 . . . . . . . . . . . 12
35 endomtr 7168 . . . . . . . . . . . 12
3617, 34, 35syl2anc 644 . . . . . . . . . . 11
37 elharval 7534 . . . . . . . . . . 11 har
3815, 36, 37sylanbrc 647 . . . . . . . . . 10 har
39 pwfseqlem5.n . . . . . . . . . . 11 har
4039adantr 453 . . . . . . . . . 10 har
41 cardom 7878 . . . . . . . . . . . 12
42 simprr 735 . . . . . . . . . . . . . . 15
434, 42sylan2b 463 . . . . . . . . . . . . . 14
4417ensymd 7161 . . . . . . . . . . . . . 14
45 domentr 7169 . . . . . . . . . . . . . 14
4643, 44, 45syl2anc 644 . . . . . . . . . . . . 13
47 omelon 7604 . . . . . . . . . . . . . . 15
48 onenon 7841 . . . . . . . . . . . . . . 15
4947, 48ax-mp 5 . . . . . . . . . . . . . 14
50 onenon 7841 . . . . . . . . . . . . . . 15
5114, 50mp1i 12 . . . . . . . . . . . . . 14
52 carddom2 7869 . . . . . . . . . . . . . 14
5349, 51, 52sylancr 646 . . . . . . . . . . . . 13
5446, 53mpbird 225 . . . . . . . . . . . 12
5541, 54syl5eqssr 3395 . . . . . . . . . . 11
56 cardonle 7849 . . . . . . . . . . . 12
5715, 56syl 16 . . . . . . . . . . 11
5855, 57sstrd 3360 . . . . . . . . . 10
59 sseq2 3372 . . . . . . . . . . . 12
60 fveq2 5731 . . . . . . . . . . . . . 14
61 f1oeq1 5668 . . . . . . . . . . . . . 14
6260, 61syl 16 . . . . . . . . . . . . 13
63 xpeq12 4900 . . . . . . . . . . . . . . 15
6463anidms 628 . . . . . . . . . . . . . 14
65 f1oeq2 5669 . . . . . . . . . . . . . 14
6664, 65syl 16 . . . . . . . . . . . . 13
67 f1oeq3 5670 . . . . . . . . . . . . 13
6862, 66, 673bitrd 272 . . . . . . . . . . . 12
6959, 68imbi12d 313 . . . . . . . . . . 11
7069rspcv 3050 . . . . . . . . . 10 har har
7138, 40, 58, 70syl3c 60 . . . . . . . . 9
72 f1oco 5701 . . . . . . . . 9
7312, 71, 72syl2anc 644 . . . . . . . 8
74 f1of 5677 . . . . . . . . . . . . . . 15
7512, 74syl 16 . . . . . . . . . . . . . 14
7675feqmptd 5782 . . . . . . . . . . . . 13
77 f1oeq1 5668 . . . . . . . . . . . . 13
7876, 77syl 16 . . . . . . . . . . . 12
7912, 78mpbid 203 . . . . . . . . . . 11
8075feqmptd 5782 . . . . . . . . . . . . 13
81 f1oeq1 5668 . . . . . . . . . . . . 13
8280, 81syl 16 . . . . . . . . . . . 12
8312, 82mpbid 203 . . . . . . . . . . 11
8479, 83xpf1o 7272 . . . . . . . . . 10
85 pwfseqlem5.t . . . . . . . . . . 11
86 f1oeq1 5668 . . . . . . . . . . 11
8785, 86ax-mp 5 . . . . . . . . . 10
8884, 87sylibr 205 . . . . . . . . 9
89 f1ocnv 5690 . . . . . . . . 9
9088, 89syl 16 . . . . . . . 8
91 f1oco 5701 . . . . . . . 8
9273, 90, 91syl2anc 644 . . . . . . 7
93 pwfseqlem5.p . . . . . . . 8
94 f1oeq1 5668 . . . . . . . 8
9593, 94ax-mp 5 . . . . . . 7
9692, 95sylibr 205 . . . . . 6
97 f1of1 5676 . . . . . 6
9896, 97syl 16 . . . . 5
99 f1of1 5676 . . . . . . . . . . . . 13
10012, 99syl 16 . . . . . . . . . . . 12
101 f1ssres 5649 . . . . . . . . . . . 12
102100, 58, 101syl2anc 644 . . . . . . . . . . 11
103 f1f1orn 5688 . . . . . . . . . . 11
104102, 103syl 16 . . . . . . . . . 10
10575, 58feqresmpt 5783 . . . . . . . . . . 11
106 f1oeq1 5668 . . . . . . . . . . 11
107105, 106syl 16 . . . . . . . . . 10
108104, 107mpbid 203 . . . . . . . . 9
109 mptresid 5198 . . . . . . . . . 10
110 f1oi 5716 . . . . . . . . . . 11
111 f1oeq1 5668 . . . . . . . . . . 11
112110, 111mpbiri 226 . . . . . . . . . 10
113109, 112mp1i 12 . . . . . . . . 9
114108, 113xpf1o 7272 . . . . . . . 8
115 pwfseqlem5.i . . . . . . . . 9
116 f1oeq1 5668 . . . . . . . . 9
117115, 116ax-mp 5 . . . . . . . 8
118114, 117sylibr 205 . . . . . . 7
119 f1of1 5676 . . . . . . 7
120118, 119syl 16 . . . . . 6
121 f1f 5642 . . . . . . 7
122 frn 5600 . . . . . . 7
123 xpss1 4987 . . . . . . 7
124102, 121, 122, 1234syl 20 . . . . . 6
125 f1ss 5647 . . . . . 6
126120, 124, 125syl2anc 644 . . . . 5
127 f1co 5651 . . . . 5
12898, 126, 127syl2anc 644 . . . 4
1295a1i 11 . . . . 5
130 peano1 4867 . . . . . . . 8
131130a1i 11 . . . . . . 7
13258, 131sseldd 3351 . . . . . 6
13375, 132ffvelrnd 5874 . . . . 5
134 pwfseqlem5.s . . . . 5 seq𝜔
135 pwfseqlem5.q . . . . 5
136129, 133, 96, 134, 135fseqenlem2 7911 . . . 4
137 f1co 5651 . . . 4
138128, 136, 137syl2anc 644 . . 3
139 pwfseqlem5.k . . . 4
140 f1eq1 5637 . . . 4
141139, 140ax-mp 5 . . 3
142138, 141sylibr 205 . 2
143 eqid 2438 . 2
144 eqid 2438 . 2
145 eqid 2438 . . 3
146145fpwwe2cbv 8510 . 2
147 eqid 2438 . 2
1481, 2, 3, 4, 142, 143, 144, 146, 147pwfseqlem4 8542 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360   w3a 937   wceq 1653   wcel 1726  wral 2707  crab 2711  cvv 2958  wsbc 3163   cin 3321   wss 3322  c0 3630  cif 3741  cpw 3801  csn 3816  cop 3819  cuni 4017  cint 4052  ciun 4095   class class class wbr 4215  copab 4268   cmpt 4269   cep 4495   cid 4496   wwe 4543  con0 4584   csuc 4586  com 4848   cxp 4879  ccnv 4880   cdm 4881   crn 4882   cres 4883  cima 4884   ccom 4885  wf 5453  wf1 5454  wf1o 5456  cfv 5457   wiso 5458  (class class class)co 6084   cmpt2 6086  seq𝜔cseqom 6707   cmap 7021   cen 7109   cdom 7110   csdm 7111  cfn 7112  OrdIsocoi 7481  harchar 7527  ccrd 7827 This theorem is referenced by:  pwfseq  8544 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-inf2 7599 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-se 4545  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-isom 5466  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6352  df-2nd 6353  df-riota 6552  df-recs 6636  df-rdg 6671  df-seqom 6708  df-1o 6727  df-er 6908  df-map 7023  df-en 7113  df-dom 7114  df-sdom 7115  df-fin 7116  df-oi 7482  df-har 7529  df-card 7831
 Copyright terms: Public domain W3C validator