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

Theorem pwfseqlem5 9883
Description: Lemma for pwfseq 9884. Although in some ways pwfseqlem4 9882 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 9247. 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 9234. 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 8963), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 9238). (Contributed by Mario Carneiro, 31-May-2015.)

Hypotheses
Ref Expression
pwfseqlem5.g (𝜑𝐺:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛))
pwfseqlem5.x (𝜑𝑋𝐴)
pwfseqlem5.h (𝜑𝐻:ω–1-1-onto𝑋)
pwfseqlem5.ps (𝜓 ↔ ((𝑡𝐴𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡))
pwfseqlem5.n (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
pwfseqlem5.o 𝑂 = OrdIso(𝑟, 𝑡)
pwfseqlem5.t 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂𝑢), (𝑂𝑣)⟩)
pwfseqlem5.p 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ 𝑇)
pwfseqlem5.s 𝑆 = seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡𝑚 suc 𝑘) ↦ ((𝑓‘(𝑥𝑘))𝑃(𝑥𝑘)))), {⟨∅, (𝑂‘∅)⟩})
pwfseqlem5.q 𝑄 = (𝑦 𝑛 ∈ ω (𝑡𝑚 𝑛) ↦ ⟨dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)⟩)
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 (𝜑𝐺:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛))
2 pwfseqlem5.x . 2 (𝜑𝑋𝐴)
3 pwfseqlem5.h . 2 (𝜑𝐻:ω–1-1-onto𝑋)
4 pwfseqlem5.ps . 2 (𝜓 ↔ ((𝑡𝐴𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡))
5 vex 3418 . . . . . . . . . . 11 𝑡 ∈ V
6 simprl3 1200 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑡𝐴𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑟 We 𝑡)
74, 6sylan2b 584 . . . . . . . . . . 11 ((𝜑𝜓) → 𝑟 We 𝑡)
8 pwfseqlem5.o . . . . . . . . . . . 12 𝑂 = OrdIso(𝑟, 𝑡)
98oiiso 8796 . . . . . . . . . . 11 ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
105, 7, 9sylancr 578 . . . . . . . . . 10 ((𝜑𝜓) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
11 isof1o 6899 . . . . . . . . . 10 (𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡) → 𝑂:dom 𝑂1-1-onto𝑡)
1210, 11syl 17 . . . . . . . . 9 ((𝜑𝜓) → 𝑂:dom 𝑂1-1-onto𝑡)
13 cardom 9209 . . . . . . . . . . . 12 (card‘ω) = ω
14 simprr 760 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑡𝐴𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → ω ≼ 𝑡)
154, 14sylan2b 584 . . . . . . . . . . . . . 14 ((𝜑𝜓) → ω ≼ 𝑡)
168oien 8797 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → dom 𝑂𝑡)
175, 7, 16sylancr 578 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → dom 𝑂𝑡)
1817ensymd 8357 . . . . . . . . . . . . . 14 ((𝜑𝜓) → 𝑡 ≈ dom 𝑂)
19 domentr 8365 . . . . . . . . . . . . . 14 ((ω ≼ 𝑡𝑡 ≈ dom 𝑂) → ω ≼ dom 𝑂)
2015, 18, 19syl2anc 576 . . . . . . . . . . . . 13 ((𝜑𝜓) → ω ≼ dom 𝑂)
21 omelon 8903 . . . . . . . . . . . . . . 15 ω ∈ On
22 onenon 9172 . . . . . . . . . . . . . . 15 (ω ∈ On → ω ∈ dom card)
2321, 22ax-mp 5 . . . . . . . . . . . . . 14 ω ∈ dom card
248oion 8795 . . . . . . . . . . . . . . . 16 (𝑡 ∈ V → dom 𝑂 ∈ On)
2524elv 3420 . . . . . . . . . . . . . . 15 dom 𝑂 ∈ On
26 onenon 9172 . . . . . . . . . . . . . . 15 (dom 𝑂 ∈ On → dom 𝑂 ∈ dom card)
2725, 26mp1i 13 . . . . . . . . . . . . . 14 ((𝜑𝜓) → dom 𝑂 ∈ dom card)
28 carddom2 9200 . . . . . . . . . . . . . 14 ((ω ∈ dom card ∧ dom 𝑂 ∈ dom card) → ((card‘ω) ⊆ (card‘dom 𝑂) ↔ ω ≼ dom 𝑂))
2923, 27, 28sylancr 578 . . . . . . . . . . . . 13 ((𝜑𝜓) → ((card‘ω) ⊆ (card‘dom 𝑂) ↔ ω ≼ dom 𝑂))
3020, 29mpbird 249 . . . . . . . . . . . 12 ((𝜑𝜓) → (card‘ω) ⊆ (card‘dom 𝑂))
3113, 30syl5eqssr 3906 . . . . . . . . . . 11 ((𝜑𝜓) → ω ⊆ (card‘dom 𝑂))
32 cardonle 9180 . . . . . . . . . . . 12 (dom 𝑂 ∈ On → (card‘dom 𝑂) ⊆ dom 𝑂)
3325, 32mp1i 13 . . . . . . . . . . 11 ((𝜑𝜓) → (card‘dom 𝑂) ⊆ dom 𝑂)
3431, 33sstrd 3868 . . . . . . . . . 10 ((𝜑𝜓) → ω ⊆ dom 𝑂)
35 sseq2 3883 . . . . . . . . . . . 12 (𝑏 = dom 𝑂 → (ω ⊆ 𝑏 ↔ ω ⊆ dom 𝑂))
36 fveq2 6499 . . . . . . . . . . . . . 14 (𝑏 = dom 𝑂 → (𝑁𝑏) = (𝑁‘dom 𝑂))
37 f1oeq1 6433 . . . . . . . . . . . . . 14 ((𝑁𝑏) = (𝑁‘dom 𝑂) → ((𝑁𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto𝑏))
3836, 37syl 17 . . . . . . . . . . . . 13 (𝑏 = dom 𝑂 → ((𝑁𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto𝑏))
39 xpeq12 5432 . . . . . . . . . . . . . . 15 ((𝑏 = dom 𝑂𝑏 = dom 𝑂) → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
4039anidms 559 . . . . . . . . . . . . . 14 (𝑏 = dom 𝑂 → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
4140f1oeq2d 6440 . . . . . . . . . . . . 13 (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto𝑏))
42 f1oeq3 6435 . . . . . . . . . . . . 13 (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
4338, 41, 423bitrd 297 . . . . . . . . . . . 12 (𝑏 = dom 𝑂 → ((𝑁𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
4435, 43imbi12d 337 . . . . . . . . . . 11 (𝑏 = dom 𝑂 → ((ω ⊆ 𝑏 → (𝑁𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) ↔ (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂)))
45 pwfseqlem5.n . . . . . . . . . . . 12 (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
4645adantr 473 . . . . . . . . . . 11 ((𝜑𝜓) → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
4725a1i 11 . . . . . . . . . . . 12 ((𝜑𝜓) → dom 𝑂 ∈ On)
481adantr 473 . . . . . . . . . . . . . . . . 17 ((𝜑𝜓) → 𝐺:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛))
49 omex 8900 . . . . . . . . . . . . . . . . . 18 ω ∈ V
50 ovex 7008 . . . . . . . . . . . . . . . . . 18 (𝐴𝑚 𝑛) ∈ V
5149, 50iunex 7481 . . . . . . . . . . . . . . . . 17 𝑛 ∈ ω (𝐴𝑚 𝑛) ∈ V
52 f1dmex 7470 . . . . . . . . . . . . . . . . 17 ((𝐺:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛) ∧ 𝑛 ∈ ω (𝐴𝑚 𝑛) ∈ V) → 𝒫 𝐴 ∈ V)
5348, 51, 52sylancl 577 . . . . . . . . . . . . . . . 16 ((𝜑𝜓) → 𝒫 𝐴 ∈ V)
54 pwexb 7305 . . . . . . . . . . . . . . . 16 (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
5553, 54sylibr 226 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → 𝐴 ∈ V)
56 simprl1 1198 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑡𝐴𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑡𝐴)
574, 56sylan2b 584 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → 𝑡𝐴)
58 ssdomg 8352 . . . . . . . . . . . . . . 15 (𝐴 ∈ V → (𝑡𝐴𝑡𝐴))
5955, 57, 58sylc 65 . . . . . . . . . . . . . 14 ((𝜑𝜓) → 𝑡𝐴)
60 canth2g 8467 . . . . . . . . . . . . . . 15 (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
61 sdomdom 8334 . . . . . . . . . . . . . . 15 (𝐴 ≺ 𝒫 𝐴𝐴 ≼ 𝒫 𝐴)
6255, 60, 613syl 18 . . . . . . . . . . . . . 14 ((𝜑𝜓) → 𝐴 ≼ 𝒫 𝐴)
63 domtr 8359 . . . . . . . . . . . . . 14 ((𝑡𝐴𝐴 ≼ 𝒫 𝐴) → 𝑡 ≼ 𝒫 𝐴)
6459, 62, 63syl2anc 576 . . . . . . . . . . . . 13 ((𝜑𝜓) → 𝑡 ≼ 𝒫 𝐴)
65 endomtr 8364 . . . . . . . . . . . . 13 ((dom 𝑂𝑡𝑡 ≼ 𝒫 𝐴) → dom 𝑂 ≼ 𝒫 𝐴)
6617, 64, 65syl2anc 576 . . . . . . . . . . . 12 ((𝜑𝜓) → dom 𝑂 ≼ 𝒫 𝐴)
67 elharval 8822 . . . . . . . . . . . 12 (dom 𝑂 ∈ (har‘𝒫 𝐴) ↔ (dom 𝑂 ∈ On ∧ dom 𝑂 ≼ 𝒫 𝐴))
6847, 66, 67sylanbrc 575 . . . . . . . . . . 11 ((𝜑𝜓) → dom 𝑂 ∈ (har‘𝒫 𝐴))
6944, 46, 68rspcdva 3541 . . . . . . . . . 10 ((𝜑𝜓) → (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
7034, 69mpd 15 . . . . . . . . 9 ((𝜑𝜓) → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂)
71 f1oco 6466 . . . . . . . . 9 ((𝑂:dom 𝑂1-1-onto𝑡 ∧ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto𝑡)
7212, 70, 71syl2anc 576 . . . . . . . 8 ((𝜑𝜓) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto𝑡)
73 f1of 6444 . . . . . . . . . . . . . . 15 (𝑂:dom 𝑂1-1-onto𝑡𝑂:dom 𝑂𝑡)
7412, 73syl 17 . . . . . . . . . . . . . 14 ((𝜑𝜓) → 𝑂:dom 𝑂𝑡)
7574feqmptd 6562 . . . . . . . . . . . . 13 ((𝜑𝜓) → 𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂𝑢)))
76 f1oeq1 6433 . . . . . . . . . . . . 13 (𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂𝑢)) → (𝑂:dom 𝑂1-1-onto𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂𝑢)):dom 𝑂1-1-onto𝑡))
7775, 76syl 17 . . . . . . . . . . . 12 ((𝜑𝜓) → (𝑂:dom 𝑂1-1-onto𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂𝑢)):dom 𝑂1-1-onto𝑡))
7812, 77mpbid 224 . . . . . . . . . . 11 ((𝜑𝜓) → (𝑢 ∈ dom 𝑂 ↦ (𝑂𝑢)):dom 𝑂1-1-onto𝑡)
7974feqmptd 6562 . . . . . . . . . . . . 13 ((𝜑𝜓) → 𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂𝑣)))
80 f1oeq1 6433 . . . . . . . . . . . . 13 (𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂𝑣)) → (𝑂:dom 𝑂1-1-onto𝑡 ↔ (𝑣 ∈ dom 𝑂 ↦ (𝑂𝑣)):dom 𝑂1-1-onto𝑡))
8179, 80syl 17 . . . . . . . . . . . 12 ((𝜑𝜓) → (𝑂:dom 𝑂1-1-onto𝑡 ↔ (𝑣 ∈ dom 𝑂 ↦ (𝑂𝑣)):dom 𝑂1-1-onto𝑡))
8212, 81mpbid 224 . . . . . . . . . . 11 ((𝜑𝜓) → (𝑣 ∈ dom 𝑂 ↦ (𝑂𝑣)):dom 𝑂1-1-onto𝑡)
8378, 82xpf1o 8475 . . . . . . . . . 10 ((𝜑𝜓) → (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂𝑢), (𝑂𝑣)⟩):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
84 pwfseqlem5.t . . . . . . . . . . 11 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂𝑢), (𝑂𝑣)⟩)
85 f1oeq1 6433 . . . . . . . . . . 11 (𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂𝑢), (𝑂𝑣)⟩) → (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) ↔ (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂𝑢), (𝑂𝑣)⟩):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡)))
8684, 85ax-mp 5 . . . . . . . . . 10 (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) ↔ (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂𝑢), (𝑂𝑣)⟩):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
8783, 86sylibr 226 . . . . . . . . 9 ((𝜑𝜓) → 𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
88 f1ocnv 6456 . . . . . . . . 9 (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) → 𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
8987, 88syl 17 . . . . . . . 8 ((𝜑𝜓) → 𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
90 f1oco 6466 . . . . . . . 8 (((𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto𝑡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂)) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ 𝑇):(𝑡 × 𝑡)–1-1-onto𝑡)
9172, 89, 90syl2anc 576 . . . . . . 7 ((𝜑𝜓) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ 𝑇):(𝑡 × 𝑡)–1-1-onto𝑡)
92 pwfseqlem5.p . . . . . . . 8 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ 𝑇)
93 f1oeq1 6433 . . . . . . . 8 (𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ 𝑇) → (𝑃:(𝑡 × 𝑡)–1-1-onto𝑡 ↔ ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ 𝑇):(𝑡 × 𝑡)–1-1-onto𝑡))
9492, 93ax-mp 5 . . . . . . 7 (𝑃:(𝑡 × 𝑡)–1-1-onto𝑡 ↔ ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ 𝑇):(𝑡 × 𝑡)–1-1-onto𝑡)
9591, 94sylibr 226 . . . . . 6 ((𝜑𝜓) → 𝑃:(𝑡 × 𝑡)–1-1-onto𝑡)
96 f1of1 6443 . . . . . 6 (𝑃:(𝑡 × 𝑡)–1-1-onto𝑡𝑃:(𝑡 × 𝑡)–1-1𝑡)
9795, 96syl 17 . . . . 5 ((𝜑𝜓) → 𝑃:(𝑡 × 𝑡)–1-1𝑡)
98 f1of1 6443 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto𝑡𝑂:dom 𝑂1-1𝑡)
9912, 98syl 17 . . . . . . . . . . . 12 ((𝜑𝜓) → 𝑂:dom 𝑂1-1𝑡)
100 f1ssres 6411 . . . . . . . . . . . 12 ((𝑂:dom 𝑂1-1𝑡 ∧ ω ⊆ dom 𝑂) → (𝑂 ↾ ω):ω–1-1𝑡)
10199, 34, 100syl2anc 576 . . . . . . . . . . 11 ((𝜑𝜓) → (𝑂 ↾ ω):ω–1-1𝑡)
102 f1f1orn 6455 . . . . . . . . . . 11 ((𝑂 ↾ ω):ω–1-1𝑡 → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
103101, 102syl 17 . . . . . . . . . 10 ((𝜑𝜓) → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
10474, 34feqresmpt 6563 . . . . . . . . . . 11 ((𝜑𝜓) → (𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂𝑥)))
105 f1oeq1 6433 . . . . . . . . . . 11 ((𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂𝑥)) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω)))
106104, 105syl 17 . . . . . . . . . 10 ((𝜑𝜓) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω)))
107103, 106mpbid 224 . . . . . . . . 9 ((𝜑𝜓) → (𝑥 ∈ ω ↦ (𝑂𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω))
108 mptresid 5762 . . . . . . . . . 10 (𝑦𝑡𝑦) = ( I ↾ 𝑡)
109 f1oi 6481 . . . . . . . . . . 11 ( I ↾ 𝑡):𝑡1-1-onto𝑡
110 f1oeq1 6433 . . . . . . . . . . 11 ((𝑦𝑡𝑦) = ( I ↾ 𝑡) → ((𝑦𝑡𝑦):𝑡1-1-onto𝑡 ↔ ( I ↾ 𝑡):𝑡1-1-onto𝑡))
111109, 110mpbiri 250 . . . . . . . . . 10 ((𝑦𝑡𝑦) = ( I ↾ 𝑡) → (𝑦𝑡𝑦):𝑡1-1-onto𝑡)
112108, 111mp1i 13 . . . . . . . . 9 ((𝜑𝜓) → (𝑦𝑡𝑦):𝑡1-1-onto𝑡)
113107, 112xpf1o 8475 . . . . . . . 8 ((𝜑𝜓) → (𝑥 ∈ ω, 𝑦𝑡 ↦ ⟨(𝑂𝑥), 𝑦⟩):(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
114 pwfseqlem5.i . . . . . . . . 9 𝐼 = (𝑥 ∈ ω, 𝑦𝑡 ↦ ⟨(𝑂𝑥), 𝑦⟩)
115 f1oeq1 6433 . . . . . . . . 9 (𝐼 = (𝑥 ∈ ω, 𝑦𝑡 ↦ ⟨(𝑂𝑥), 𝑦⟩) → (𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡) ↔ (𝑥 ∈ ω, 𝑦𝑡 ↦ ⟨(𝑂𝑥), 𝑦⟩):(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡)))
116114, 115ax-mp 5 . . . . . . . 8 (𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡) ↔ (𝑥 ∈ ω, 𝑦𝑡 ↦ ⟨(𝑂𝑥), 𝑦⟩):(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
117113, 116sylibr 226 . . . . . . 7 ((𝜑𝜓) → 𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
118 f1of1 6443 . . . . . . 7 (𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
119117, 118syl 17 . . . . . 6 ((𝜑𝜓) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
120 f1f 6404 . . . . . . 7 ((𝑂 ↾ ω):ω–1-1𝑡 → (𝑂 ↾ ω):ω⟶𝑡)
121 frn 6350 . . . . . . 7 ((𝑂 ↾ ω):ω⟶𝑡 → ran (𝑂 ↾ ω) ⊆ 𝑡)
122 xpss1 5426 . . . . . . 7 (ran (𝑂 ↾ ω) ⊆ 𝑡 → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
123101, 120, 121, 1224syl 19 . . . . . 6 ((𝜑𝜓) → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
124 f1ss 6409 . . . . . 6 ((𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡) ∧ (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
125119, 123, 124syl2anc 576 . . . . 5 ((𝜑𝜓) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
126 f1co 6414 . . . . 5 ((𝑃:(𝑡 × 𝑡)–1-1𝑡𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) → (𝑃𝐼):(ω × 𝑡)–1-1𝑡)
12797, 125, 126syl2anc 576 . . . 4 ((𝜑𝜓) → (𝑃𝐼):(ω × 𝑡)–1-1𝑡)
1285a1i 11 . . . . 5 ((𝜑𝜓) → 𝑡 ∈ V)
129 peano1 7416 . . . . . . . 8 ∅ ∈ ω
130129a1i 11 . . . . . . 7 ((𝜑𝜓) → ∅ ∈ ω)
13134, 130sseldd 3859 . . . . . 6 ((𝜑𝜓) → ∅ ∈ dom 𝑂)
13274, 131ffvelrnd 6677 . . . . 5 ((𝜑𝜓) → (𝑂‘∅) ∈ 𝑡)
133 pwfseqlem5.s . . . . 5 𝑆 = seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡𝑚 suc 𝑘) ↦ ((𝑓‘(𝑥𝑘))𝑃(𝑥𝑘)))), {⟨∅, (𝑂‘∅)⟩})
134 pwfseqlem5.q . . . . 5 𝑄 = (𝑦 𝑛 ∈ ω (𝑡𝑚 𝑛) ↦ ⟨dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)⟩)
135128, 132, 95, 133, 134fseqenlem2 9245 . . . 4 ((𝜑𝜓) → 𝑄: 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1→(ω × 𝑡))
136 f1co 6414 . . . 4 (((𝑃𝐼):(ω × 𝑡)–1-1𝑡𝑄: 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1→(ω × 𝑡)) → ((𝑃𝐼) ∘ 𝑄): 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡)
137127, 135, 136syl2anc 576 . . 3 ((𝜑𝜓) → ((𝑃𝐼) ∘ 𝑄): 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡)
138 pwfseqlem5.k . . . 4 𝐾 = ((𝑃𝐼) ∘ 𝑄)
139 f1eq1 6399 . . . 4 (𝐾 = ((𝑃𝐼) ∘ 𝑄) → (𝐾: 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡 ↔ ((𝑃𝐼) ∘ 𝑄): 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡))
140138, 139ax-mp 5 . . 3 (𝐾: 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡 ↔ ((𝑃𝐼) ∘ 𝑄): 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡)
141137, 140sylibr 226 . 2 ((𝜑𝜓) → 𝐾: 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡)
142 eqid 2778 . 2 (𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))}) = (𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})
143 eqid 2778 . 2 (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡}))) = (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))
144 eqid 2778 . . 3 {⟨𝑐, 𝑑⟩ ∣ ((𝑐𝐴𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚𝑐 [(𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑐, 𝑑⟩ ∣ ((𝑐𝐴𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚𝑐 [(𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))}
145144fpwwe2cbv 9850 . 2 {⟨𝑐, 𝑑⟩ ∣ ((𝑐𝐴𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚𝑐 [(𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏𝑎 [(𝑠 “ {𝑏}) / 𝑤](𝑤(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))(𝑠 ∩ (𝑤 × 𝑤))) = 𝑏))}
146 eqid 2778 . 2 dom {⟨𝑐, 𝑑⟩ ∣ ((𝑐𝐴𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚𝑐 [(𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = dom {⟨𝑐, 𝑑⟩ ∣ ((𝑐𝐴𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚𝑐 [(𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))}
1471, 2, 3, 4, 141, 142, 143, 145, 146pwfseqlem4 9882 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2050  wral 3088  {crab 3092  Vcvv 3415  [wsbc 3681  cin 3828  wss 3829  c0 4178  ifcif 4350  𝒫 cpw 4422  {csn 4441  cop 4447   cuni 4712   cint 4749   ciun 4792   class class class wbr 4929  {copab 4991  cmpt 5008   I cid 5311   E cep 5316   We wwe 5365   × cxp 5405  ccnv 5406  dom cdm 5407  ran crn 5408  cres 5409  cima 5410  ccom 5411  Oncon0 6029  suc csuc 6031  wf 6184  1-1wf1 6185  1-1-ontowf1o 6187  cfv 6188   Isom wiso 6189  (class class class)co 6976  cmpo 6978  ωcom 7396  seq𝜔cseqom 7886  𝑚 cmap 8206  cen 8303  cdom 8304  csdm 8305  Fincfn 8306  OrdIsocoi 8768  harchar 8815  cardccrd 9158
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-inf2 8898
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-se 5367  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-isom 6197  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-om 7397  df-1st 7501  df-2nd 7502  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-seqom 7887  df-1o 7905  df-er 8089  df-map 8208  df-en 8307  df-dom 8308  df-sdom 8309  df-fin 8310  df-oi 8769  df-har 8817  df-card 9162
This theorem is referenced by:  pwfseq  9884
  Copyright terms: Public domain W3C validator