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

Theorem pwfseqlem5 9685
Description: Lemma for pwfseq 9686. Although in some ways pwfseqlem4 9684 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 9048. 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 9035. 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 8765), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 9039). (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 3351 . . . . . . . . . . 11 𝑡 ∈ V
6 simprl3 1268 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑡𝐴𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑟 We 𝑡)
74, 6sylan2b 494 . . . . . . . . . . 11 ((𝜑𝜓) → 𝑟 We 𝑡)
8 pwfseqlem5.o . . . . . . . . . . . 12 𝑂 = OrdIso(𝑟, 𝑡)
98oiiso 8596 . . . . . . . . . . 11 ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
105, 7, 9sylancr 695 . . . . . . . . . 10 ((𝜑𝜓) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡))
11 isof1o 6714 . . . . . . . . . 10 (𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡) → 𝑂:dom 𝑂1-1-onto𝑡)
1210, 11syl 17 . . . . . . . . 9 ((𝜑𝜓) → 𝑂:dom 𝑂1-1-onto𝑡)
13 cardom 9010 . . . . . . . . . . . 12 (card‘ω) = ω
14 simprr 810 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑡𝐴𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → ω ≼ 𝑡)
154, 14sylan2b 494 . . . . . . . . . . . . . 14 ((𝜑𝜓) → ω ≼ 𝑡)
168oien 8597 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → dom 𝑂𝑡)
175, 7, 16sylancr 695 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → dom 𝑂𝑡)
1817ensymd 8158 . . . . . . . . . . . . . 14 ((𝜑𝜓) → 𝑡 ≈ dom 𝑂)
19 domentr 8166 . . . . . . . . . . . . . 14 ((ω ≼ 𝑡𝑡 ≈ dom 𝑂) → ω ≼ dom 𝑂)
2015, 18, 19syl2anc 693 . . . . . . . . . . . . 13 ((𝜑𝜓) → ω ≼ dom 𝑂)
21 omelon 8705 . . . . . . . . . . . . . . 15 ω ∈ On
22 onenon 8973 . . . . . . . . . . . . . . 15 (ω ∈ On → ω ∈ dom card)
2321, 22ax-mp 5 . . . . . . . . . . . . . 14 ω ∈ dom card
248oion 8595 . . . . . . . . . . . . . . . 16 (𝑡 ∈ V → dom 𝑂 ∈ On)
255, 24ax-mp 5 . . . . . . . . . . . . . . 15 dom 𝑂 ∈ On
26 onenon 8973 . . . . . . . . . . . . . . 15 (dom 𝑂 ∈ On → dom 𝑂 ∈ dom card)
2725, 26mp1i 13 . . . . . . . . . . . . . 14 ((𝜑𝜓) → dom 𝑂 ∈ dom card)
28 carddom2 9001 . . . . . . . . . . . . . 14 ((ω ∈ dom card ∧ dom 𝑂 ∈ dom card) → ((card‘ω) ⊆ (card‘dom 𝑂) ↔ ω ≼ dom 𝑂))
2923, 27, 28sylancr 695 . . . . . . . . . . . . 13 ((𝜑𝜓) → ((card‘ω) ⊆ (card‘dom 𝑂) ↔ ω ≼ dom 𝑂))
3020, 29mpbird 247 . . . . . . . . . . . 12 ((𝜑𝜓) → (card‘ω) ⊆ (card‘dom 𝑂))
3113, 30syl5eqssr 3796 . . . . . . . . . . 11 ((𝜑𝜓) → ω ⊆ (card‘dom 𝑂))
3225a1i 11 . . . . . . . . . . . 12 ((𝜑𝜓) → dom 𝑂 ∈ On)
33 cardonle 8981 . . . . . . . . . . . 12 (dom 𝑂 ∈ On → (card‘dom 𝑂) ⊆ dom 𝑂)
3432, 33syl 17 . . . . . . . . . . 11 ((𝜑𝜓) → (card‘dom 𝑂) ⊆ dom 𝑂)
3531, 34sstrd 3759 . . . . . . . . . 10 ((𝜑𝜓) → ω ⊆ dom 𝑂)
36 sseq2 3773 . . . . . . . . . . . 12 (𝑏 = dom 𝑂 → (ω ⊆ 𝑏 ↔ ω ⊆ dom 𝑂))
37 fveq2 6331 . . . . . . . . . . . . . 14 (𝑏 = dom 𝑂 → (𝑁𝑏) = (𝑁‘dom 𝑂))
38 f1oeq1 6267 . . . . . . . . . . . . . 14 ((𝑁𝑏) = (𝑁‘dom 𝑂) → ((𝑁𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto𝑏))
3937, 38syl 17 . . . . . . . . . . . . 13 (𝑏 = dom 𝑂 → ((𝑁𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto𝑏))
40 xpeq12 5273 . . . . . . . . . . . . . . 15 ((𝑏 = dom 𝑂𝑏 = dom 𝑂) → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
4140anidms 677 . . . . . . . . . . . . . 14 (𝑏 = dom 𝑂 → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂))
42 f1oeq2 6268 . . . . . . . . . . . . . 14 ((𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂) → ((𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto𝑏))
4341, 42syl 17 . . . . . . . . . . . . 13 (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto𝑏))
44 f1oeq3 6269 . . . . . . . . . . . . 13 (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
4539, 43, 443bitrd 294 . . . . . . . . . . . 12 (𝑏 = dom 𝑂 → ((𝑁𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
4636, 45imbi12d 333 . . . . . . . . . . 11 (𝑏 = dom 𝑂 → ((ω ⊆ 𝑏 → (𝑁𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) ↔ (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂)))
47 pwfseqlem5.n . . . . . . . . . . . 12 (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
4847adantr 473 . . . . . . . . . . 11 ((𝜑𝜓) → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
491adantr 473 . . . . . . . . . . . . . . . . 17 ((𝜑𝜓) → 𝐺:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛))
50 omex 8702 . . . . . . . . . . . . . . . . . 18 ω ∈ V
51 ovex 6821 . . . . . . . . . . . . . . . . . 18 (𝐴𝑚 𝑛) ∈ V
5250, 51iunex 7292 . . . . . . . . . . . . . . . . 17 𝑛 ∈ ω (𝐴𝑚 𝑛) ∈ V
53 f1dmex 7281 . . . . . . . . . . . . . . . . 17 ((𝐺:𝒫 𝐴1-1 𝑛 ∈ ω (𝐴𝑚 𝑛) ∧ 𝑛 ∈ ω (𝐴𝑚 𝑛) ∈ V) → 𝒫 𝐴 ∈ V)
5449, 52, 53sylancl 694 . . . . . . . . . . . . . . . 16 ((𝜑𝜓) → 𝒫 𝐴 ∈ V)
55 pwexb 7120 . . . . . . . . . . . . . . . 16 (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
5654, 55sylibr 224 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → 𝐴 ∈ V)
57 simprl1 1264 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑡𝐴𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑡𝐴)
584, 57sylan2b 494 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → 𝑡𝐴)
59 ssdomg 8153 . . . . . . . . . . . . . . 15 (𝐴 ∈ V → (𝑡𝐴𝑡𝐴))
6056, 58, 59sylc 65 . . . . . . . . . . . . . 14 ((𝜑𝜓) → 𝑡𝐴)
61 canth2g 8268 . . . . . . . . . . . . . . 15 (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
62 sdomdom 8135 . . . . . . . . . . . . . . 15 (𝐴 ≺ 𝒫 𝐴𝐴 ≼ 𝒫 𝐴)
6356, 61, 623syl 18 . . . . . . . . . . . . . 14 ((𝜑𝜓) → 𝐴 ≼ 𝒫 𝐴)
64 domtr 8160 . . . . . . . . . . . . . 14 ((𝑡𝐴𝐴 ≼ 𝒫 𝐴) → 𝑡 ≼ 𝒫 𝐴)
6560, 63, 64syl2anc 693 . . . . . . . . . . . . 13 ((𝜑𝜓) → 𝑡 ≼ 𝒫 𝐴)
66 endomtr 8165 . . . . . . . . . . . . 13 ((dom 𝑂𝑡𝑡 ≼ 𝒫 𝐴) → dom 𝑂 ≼ 𝒫 𝐴)
6717, 65, 66syl2anc 693 . . . . . . . . . . . 12 ((𝜑𝜓) → dom 𝑂 ≼ 𝒫 𝐴)
68 elharval 8622 . . . . . . . . . . . 12 (dom 𝑂 ∈ (har‘𝒫 𝐴) ↔ (dom 𝑂 ∈ On ∧ dom 𝑂 ≼ 𝒫 𝐴))
6932, 67, 68sylanbrc 698 . . . . . . . . . . 11 ((𝜑𝜓) → dom 𝑂 ∈ (har‘𝒫 𝐴))
7046, 48, 69rspcdva 3463 . . . . . . . . . 10 ((𝜑𝜓) → (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂))
7135, 70mpd 15 . . . . . . . . 9 ((𝜑𝜓) → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂)
72 f1oco 6299 . . . . . . . . 9 ((𝑂:dom 𝑂1-1-onto𝑡 ∧ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom 𝑂) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto𝑡)
7312, 71, 72syl2anc 693 . . . . . . . 8 ((𝜑𝜓) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto𝑡)
74 f1of 6277 . . . . . . . . . . . . . . 15 (𝑂:dom 𝑂1-1-onto𝑡𝑂:dom 𝑂𝑡)
7512, 74syl 17 . . . . . . . . . . . . . 14 ((𝜑𝜓) → 𝑂:dom 𝑂𝑡)
7675feqmptd 6390 . . . . . . . . . . . . 13 ((𝜑𝜓) → 𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂𝑢)))
77 f1oeq1 6267 . . . . . . . . . . . . 13 (𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂𝑢)) → (𝑂:dom 𝑂1-1-onto𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂𝑢)):dom 𝑂1-1-onto𝑡))
7876, 77syl 17 . . . . . . . . . . . 12 ((𝜑𝜓) → (𝑂:dom 𝑂1-1-onto𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂𝑢)):dom 𝑂1-1-onto𝑡))
7912, 78mpbid 222 . . . . . . . . . . 11 ((𝜑𝜓) → (𝑢 ∈ dom 𝑂 ↦ (𝑂𝑢)):dom 𝑂1-1-onto𝑡)
8075feqmptd 6390 . . . . . . . . . . . . 13 ((𝜑𝜓) → 𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂𝑣)))
81 f1oeq1 6267 . . . . . . . . . . . . 13 (𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂𝑣)) → (𝑂:dom 𝑂1-1-onto𝑡 ↔ (𝑣 ∈ dom 𝑂 ↦ (𝑂𝑣)):dom 𝑂1-1-onto𝑡))
8280, 81syl 17 . . . . . . . . . . . 12 ((𝜑𝜓) → (𝑂:dom 𝑂1-1-onto𝑡 ↔ (𝑣 ∈ dom 𝑂 ↦ (𝑂𝑣)):dom 𝑂1-1-onto𝑡))
8312, 82mpbid 222 . . . . . . . . . . 11 ((𝜑𝜓) → (𝑣 ∈ dom 𝑂 ↦ (𝑂𝑣)):dom 𝑂1-1-onto𝑡)
8479, 83xpf1o 8276 . . . . . . . . . 10 ((𝜑𝜓) → (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂𝑢), (𝑂𝑣)⟩):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
85 pwfseqlem5.t . . . . . . . . . . 11 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂𝑢), (𝑂𝑣)⟩)
86 f1oeq1 6267 . . . . . . . . . . 11 (𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂𝑢), (𝑂𝑣)⟩) → (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) ↔ (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂𝑢), (𝑂𝑣)⟩):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡)))
8785, 86ax-mp 5 . . . . . . . . . 10 (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) ↔ (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂𝑢), (𝑂𝑣)⟩):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
8884, 87sylibr 224 . . . . . . . . 9 ((𝜑𝜓) → 𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))
89 f1ocnv 6289 . . . . . . . . 9 (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) → 𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
9088, 89syl 17 . . . . . . . 8 ((𝜑𝜓) → 𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂))
91 f1oco 6299 . . . . . . . 8 (((𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto𝑡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom 𝑂 × dom 𝑂)) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ 𝑇):(𝑡 × 𝑡)–1-1-onto𝑡)
9273, 90, 91syl2anc 693 . . . . . . 7 ((𝜑𝜓) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ 𝑇):(𝑡 × 𝑡)–1-1-onto𝑡)
93 pwfseqlem5.p . . . . . . . 8 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ 𝑇)
94 f1oeq1 6267 . . . . . . . 8 (𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ 𝑇) → (𝑃:(𝑡 × 𝑡)–1-1-onto𝑡 ↔ ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ 𝑇):(𝑡 × 𝑡)–1-1-onto𝑡))
9593, 94ax-mp 5 . . . . . . 7 (𝑃:(𝑡 × 𝑡)–1-1-onto𝑡 ↔ ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ 𝑇):(𝑡 × 𝑡)–1-1-onto𝑡)
9692, 95sylibr 224 . . . . . 6 ((𝜑𝜓) → 𝑃:(𝑡 × 𝑡)–1-1-onto𝑡)
97 f1of1 6276 . . . . . 6 (𝑃:(𝑡 × 𝑡)–1-1-onto𝑡𝑃:(𝑡 × 𝑡)–1-1𝑡)
9896, 97syl 17 . . . . 5 ((𝜑𝜓) → 𝑃:(𝑡 × 𝑡)–1-1𝑡)
99 f1of1 6276 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto𝑡𝑂:dom 𝑂1-1𝑡)
10012, 99syl 17 . . . . . . . . . . . 12 ((𝜑𝜓) → 𝑂:dom 𝑂1-1𝑡)
101 f1ssres 6247 . . . . . . . . . . . 12 ((𝑂:dom 𝑂1-1𝑡 ∧ ω ⊆ dom 𝑂) → (𝑂 ↾ ω):ω–1-1𝑡)
102100, 35, 101syl2anc 693 . . . . . . . . . . 11 ((𝜑𝜓) → (𝑂 ↾ ω):ω–1-1𝑡)
103 f1f1orn 6288 . . . . . . . . . . 11 ((𝑂 ↾ ω):ω–1-1𝑡 → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
104102, 103syl 17 . . . . . . . . . 10 ((𝜑𝜓) → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω))
10575, 35feqresmpt 6391 . . . . . . . . . . 11 ((𝜑𝜓) → (𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂𝑥)))
106 f1oeq1 6267 . . . . . . . . . . 11 ((𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂𝑥)) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω)))
107105, 106syl 17 . . . . . . . . . 10 ((𝜑𝜓) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω)))
108104, 107mpbid 222 . . . . . . . . 9 ((𝜑𝜓) → (𝑥 ∈ ω ↦ (𝑂𝑥)):ω–1-1-onto→ran (𝑂 ↾ ω))
109 mptresid 5596 . . . . . . . . . 10 (𝑦𝑡𝑦) = ( I ↾ 𝑡)
110 f1oi 6314 . . . . . . . . . . 11 ( I ↾ 𝑡):𝑡1-1-onto𝑡
111 f1oeq1 6267 . . . . . . . . . . 11 ((𝑦𝑡𝑦) = ( I ↾ 𝑡) → ((𝑦𝑡𝑦):𝑡1-1-onto𝑡 ↔ ( I ↾ 𝑡):𝑡1-1-onto𝑡))
112110, 111mpbiri 248 . . . . . . . . . 10 ((𝑦𝑡𝑦) = ( I ↾ 𝑡) → (𝑦𝑡𝑦):𝑡1-1-onto𝑡)
113109, 112mp1i 13 . . . . . . . . 9 ((𝜑𝜓) → (𝑦𝑡𝑦):𝑡1-1-onto𝑡)
114108, 113xpf1o 8276 . . . . . . . 8 ((𝜑𝜓) → (𝑥 ∈ ω, 𝑦𝑡 ↦ ⟨(𝑂𝑥), 𝑦⟩):(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
115 pwfseqlem5.i . . . . . . . . 9 𝐼 = (𝑥 ∈ ω, 𝑦𝑡 ↦ ⟨(𝑂𝑥), 𝑦⟩)
116 f1oeq1 6267 . . . . . . . . 9 (𝐼 = (𝑥 ∈ ω, 𝑦𝑡 ↦ ⟨(𝑂𝑥), 𝑦⟩) → (𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡) ↔ (𝑥 ∈ ω, 𝑦𝑡 ↦ ⟨(𝑂𝑥), 𝑦⟩):(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡)))
117115, 116ax-mp 5 . . . . . . . 8 (𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡) ↔ (𝑥 ∈ ω, 𝑦𝑡 ↦ ⟨(𝑂𝑥), 𝑦⟩):(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
118114, 117sylibr 224 . . . . . . 7 ((𝜑𝜓) → 𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡))
119 f1of1 6276 . . . . . . 7 (𝐼:(ω × 𝑡)–1-1-onto→(ran (𝑂 ↾ ω) × 𝑡) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
120118, 119syl 17 . . . . . 6 ((𝜑𝜓) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡))
121 f1f 6240 . . . . . . 7 ((𝑂 ↾ ω):ω–1-1𝑡 → (𝑂 ↾ ω):ω⟶𝑡)
122 frn 6192 . . . . . . 7 ((𝑂 ↾ ω):ω⟶𝑡 → ran (𝑂 ↾ ω) ⊆ 𝑡)
123 xpss1 5266 . . . . . . 7 (ran (𝑂 ↾ ω) ⊆ 𝑡 → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
124102, 121, 122, 1234syl 19 . . . . . 6 ((𝜑𝜓) → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡))
125 f1ss 6245 . . . . . 6 ((𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡) ∧ (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
126120, 124, 125syl2anc 693 . . . . 5 ((𝜑𝜓) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡))
127 f1co 6250 . . . . 5 ((𝑃:(𝑡 × 𝑡)–1-1𝑡𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) → (𝑃𝐼):(ω × 𝑡)–1-1𝑡)
12898, 126, 127syl2anc 693 . . . 4 ((𝜑𝜓) → (𝑃𝐼):(ω × 𝑡)–1-1𝑡)
1295a1i 11 . . . . 5 ((𝜑𝜓) → 𝑡 ∈ V)
130 peano1 7230 . . . . . . . 8 ∅ ∈ ω
131130a1i 11 . . . . . . 7 ((𝜑𝜓) → ∅ ∈ ω)
13235, 131sseldd 3750 . . . . . 6 ((𝜑𝜓) → ∅ ∈ dom 𝑂)
13375, 132ffvelrnd 6502 . . . . 5 ((𝜑𝜓) → (𝑂‘∅) ∈ 𝑡)
134 pwfseqlem5.s . . . . 5 𝑆 = seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡𝑚 suc 𝑘) ↦ ((𝑓‘(𝑥𝑘))𝑃(𝑥𝑘)))), {⟨∅, (𝑂‘∅)⟩})
135 pwfseqlem5.q . . . . 5 𝑄 = (𝑦 𝑛 ∈ ω (𝑡𝑚 𝑛) ↦ ⟨dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)⟩)
136129, 133, 96, 134, 135fseqenlem2 9046 . . . 4 ((𝜑𝜓) → 𝑄: 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1→(ω × 𝑡))
137 f1co 6250 . . . 4 (((𝑃𝐼):(ω × 𝑡)–1-1𝑡𝑄: 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1→(ω × 𝑡)) → ((𝑃𝐼) ∘ 𝑄): 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡)
138128, 136, 137syl2anc 693 . . 3 ((𝜑𝜓) → ((𝑃𝐼) ∘ 𝑄): 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡)
139 pwfseqlem5.k . . . 4 𝐾 = ((𝑃𝐼) ∘ 𝑄)
140 f1eq1 6235 . . . 4 (𝐾 = ((𝑃𝐼) ∘ 𝑄) → (𝐾: 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡 ↔ ((𝑃𝐼) ∘ 𝑄): 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡))
141139, 140ax-mp 5 . . 3 (𝐾: 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡 ↔ ((𝑃𝐼) ∘ 𝑄): 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡)
142138, 141sylibr 224 . 2 ((𝜑𝜓) → 𝐾: 𝑛 ∈ ω (𝑡𝑚 𝑛)–1-1𝑡)
143 eqid 2769 . 2 (𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))}) = (𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})
144 eqid 2769 . 2 (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡}))) = (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))
145 eqid 2769 . . 3 {⟨𝑐, 𝑑⟩ ∣ ((𝑐𝐴𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚𝑐 [(𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑐, 𝑑⟩ ∣ ((𝑐𝐴𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚𝑐 [(𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))}
146145fpwwe2cbv 9652 . 2 {⟨𝑐, 𝑑⟩ ∣ ((𝑐𝐴𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚𝑐 [(𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏𝑎 [(𝑠 “ {𝑏}) / 𝑤](𝑤(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))(𝑠 ∩ (𝑤 × 𝑤))) = 𝑏))}
147 eqid 2769 . 2 dom {⟨𝑐, 𝑑⟩ ∣ ((𝑐𝐴𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚𝑐 [(𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = dom {⟨𝑐, 𝑑⟩ ∣ ((𝑐𝐴𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚𝑐 [(𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘ {𝑧 ∈ ω ∣ ¬ ((𝐺‘{𝑖𝑡 ∣ ((𝐾𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (𝐺‘(𝐾𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))}
1481, 2, 3, 4, 142, 143, 144, 146, 147pwfseqlem4 9684 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1069   = wceq 1629  wcel 2143  wral 3059  {crab 3063  Vcvv 3348  [wsbc 3584  cin 3719  wss 3720  c0 4060  ifcif 4222  𝒫 cpw 4294  {csn 4313  cop 4319   cuni 4571   cint 4608   ciun 4651   class class class wbr 4783  {copab 4843  cmpt 4860   I cid 5155   E cep 5160   We wwe 5206   × cxp 5246  ccnv 5247  dom cdm 5248  ran crn 5249  cres 5250  cima 5251  ccom 5252  Oncon0 5865  suc csuc 5867  wf 6026  1-1wf1 6027  1-1-ontowf1o 6029  cfv 6030   Isom wiso 6031  (class class class)co 6791  cmpt2 6793  ωcom 7210  seq𝜔cseqom 7693  𝑚 cmap 8007  cen 8104  cdom 8105  csdm 8106  Fincfn 8107  OrdIsocoi 8568  harchar 8615  cardccrd 8959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2145  ax-9 2152  ax-10 2172  ax-11 2188  ax-12 2201  ax-13 2406  ax-ext 2749  ax-rep 4901  ax-sep 4911  ax-nul 4919  ax-pow 4970  ax-pr 5033  ax-un 7094  ax-inf2 8700
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1070  df-3an 1071  df-tru 1632  df-ex 1851  df-nf 1856  df-sb 2048  df-eu 2620  df-mo 2621  df-clab 2756  df-cleq 2762  df-clel 2765  df-nfc 2900  df-ne 2942  df-ral 3064  df-rex 3065  df-reu 3066  df-rmo 3067  df-rab 3068  df-v 3350  df-sbc 3585  df-csb 3680  df-dif 3723  df-un 3725  df-in 3727  df-ss 3734  df-pss 3736  df-nul 4061  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4572  df-int 4609  df-iun 4653  df-br 4784  df-opab 4844  df-mpt 4861  df-tr 4884  df-id 5156  df-eprel 5161  df-po 5169  df-so 5170  df-fr 5207  df-se 5208  df-we 5209  df-xp 5254  df-rel 5255  df-cnv 5256  df-co 5257  df-dm 5258  df-rn 5259  df-res 5260  df-ima 5261  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-isom 6039  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-om 7211  df-1st 7313  df-2nd 7314  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-seqom 7694  df-1o 7711  df-er 7894  df-map 8009  df-en 8108  df-dom 8109  df-sdom 8110  df-fin 8111  df-oi 8569  df-har 8617  df-card 8963
This theorem is referenced by:  pwfseq  9686
  Copyright terms: Public domain W3C validator