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

Theorem pwfseqlem5 10660
Description: Lemma for pwfseq 10661. Although in some ways pwfseqlem4 10659 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 10024. 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 10011. 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 9703), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 10015). (Contributed by Mario Carneiro, 31-May-2015.)

Hypotheses
Ref Expression
pwfseqlem5.g (πœ‘ β†’ 𝐺:𝒫 𝐴–1-1β†’βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛))
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 ↦ (π‘₯ ∈ (𝑑 ↑m suc π‘˜) ↦ ((π‘“β€˜(π‘₯ β†Ύ π‘˜))𝑃(π‘₯β€˜π‘˜)))), {βŸ¨βˆ…, (π‘‚β€˜βˆ…)⟩})
pwfseqlem5.q 𝑄 = (𝑦 ∈ βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛) ↦ ⟨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β†’βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛))
2 pwfseqlem5.x . 2 (πœ‘ β†’ 𝑋 βŠ† 𝐴)
3 pwfseqlem5.h . 2 (πœ‘ β†’ 𝐻:ω–1-1-onto→𝑋)
4 pwfseqlem5.ps . 2 (πœ“ ↔ ((𝑑 βŠ† 𝐴 ∧ π‘Ÿ βŠ† (𝑑 Γ— 𝑑) ∧ π‘Ÿ We 𝑑) ∧ Ο‰ β‰Ό 𝑑))
5 vex 3478 . . . . . . . . . . 11 𝑑 ∈ V
6 simprl3 1220 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑑 βŠ† 𝐴 ∧ π‘Ÿ βŠ† (𝑑 Γ— 𝑑) ∧ π‘Ÿ We 𝑑) ∧ Ο‰ β‰Ό 𝑑)) β†’ π‘Ÿ We 𝑑)
74, 6sylan2b 594 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ π‘Ÿ We 𝑑)
8 pwfseqlem5.o . . . . . . . . . . . 12 𝑂 = OrdIso(π‘Ÿ, 𝑑)
98oiiso 9534 . . . . . . . . . . 11 ((𝑑 ∈ V ∧ π‘Ÿ We 𝑑) β†’ 𝑂 Isom E , π‘Ÿ (dom 𝑂, 𝑑))
105, 7, 9sylancr 587 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ 𝑂 Isom E , π‘Ÿ (dom 𝑂, 𝑑))
11 isof1o 7322 . . . . . . . . . 10 (𝑂 Isom E , π‘Ÿ (dom 𝑂, 𝑑) β†’ 𝑂:dom 𝑂–1-1-onto→𝑑)
1210, 11syl 17 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ 𝑂:dom 𝑂–1-1-onto→𝑑)
13 cardom 9983 . . . . . . . . . . . 12 (cardβ€˜Ο‰) = Ο‰
14 simprr 771 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ ((𝑑 βŠ† 𝐴 ∧ π‘Ÿ βŠ† (𝑑 Γ— 𝑑) ∧ π‘Ÿ We 𝑑) ∧ Ο‰ β‰Ό 𝑑)) β†’ Ο‰ β‰Ό 𝑑)
154, 14sylan2b 594 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ Ο‰ β‰Ό 𝑑)
168oien 9535 . . . . . . . . . . . . . . . 16 ((𝑑 ∈ V ∧ π‘Ÿ We 𝑑) β†’ dom 𝑂 β‰ˆ 𝑑)
175, 7, 16sylancr 587 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ dom 𝑂 β‰ˆ 𝑑)
1817ensymd 9003 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ 𝑑 β‰ˆ dom 𝑂)
19 domentr 9011 . . . . . . . . . . . . . 14 ((Ο‰ β‰Ό 𝑑 ∧ 𝑑 β‰ˆ dom 𝑂) β†’ Ο‰ β‰Ό dom 𝑂)
2015, 18, 19syl2anc 584 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ Ο‰ β‰Ό dom 𝑂)
21 omelon 9643 . . . . . . . . . . . . . . 15 Ο‰ ∈ On
22 onenon 9946 . . . . . . . . . . . . . . 15 (Ο‰ ∈ On β†’ Ο‰ ∈ dom card)
2321, 22ax-mp 5 . . . . . . . . . . . . . 14 Ο‰ ∈ dom card
248oion 9533 . . . . . . . . . . . . . . . 16 (𝑑 ∈ V β†’ dom 𝑂 ∈ On)
2524elv 3480 . . . . . . . . . . . . . . 15 dom 𝑂 ∈ On
26 onenon 9946 . . . . . . . . . . . . . . 15 (dom 𝑂 ∈ On β†’ dom 𝑂 ∈ dom card)
2725, 26mp1i 13 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ dom 𝑂 ∈ dom card)
28 carddom2 9974 . . . . . . . . . . . . . 14 ((Ο‰ ∈ dom card ∧ dom 𝑂 ∈ dom card) β†’ ((cardβ€˜Ο‰) βŠ† (cardβ€˜dom 𝑂) ↔ Ο‰ β‰Ό dom 𝑂))
2923, 27, 28sylancr 587 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ ((cardβ€˜Ο‰) βŠ† (cardβ€˜dom 𝑂) ↔ Ο‰ β‰Ό dom 𝑂))
3020, 29mpbird 256 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ (cardβ€˜Ο‰) βŠ† (cardβ€˜dom 𝑂))
3113, 30eqsstrrid 4031 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ Ο‰ βŠ† (cardβ€˜dom 𝑂))
32 cardonle 9954 . . . . . . . . . . . 12 (dom 𝑂 ∈ On β†’ (cardβ€˜dom 𝑂) βŠ† dom 𝑂)
3325, 32mp1i 13 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ (cardβ€˜dom 𝑂) βŠ† dom 𝑂)
3431, 33sstrd 3992 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ Ο‰ βŠ† dom 𝑂)
35 sseq2 4008 . . . . . . . . . . . 12 (𝑏 = dom 𝑂 β†’ (Ο‰ βŠ† 𝑏 ↔ Ο‰ βŠ† dom 𝑂))
36 fveq2 6891 . . . . . . . . . . . . . 14 (𝑏 = dom 𝑂 β†’ (π‘β€˜π‘) = (π‘β€˜dom 𝑂))
3736f1oeq1d 6828 . . . . . . . . . . . . 13 (𝑏 = dom 𝑂 β†’ ((π‘β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏 ↔ (π‘β€˜dom 𝑂):(𝑏 Γ— 𝑏)–1-1-onto→𝑏))
38 xpeq12 5701 . . . . . . . . . . . . . . 15 ((𝑏 = dom 𝑂 ∧ 𝑏 = dom 𝑂) β†’ (𝑏 Γ— 𝑏) = (dom 𝑂 Γ— dom 𝑂))
3938anidms 567 . . . . . . . . . . . . . 14 (𝑏 = dom 𝑂 β†’ (𝑏 Γ— 𝑏) = (dom 𝑂 Γ— dom 𝑂))
4039f1oeq2d 6829 . . . . . . . . . . . . 13 (𝑏 = dom 𝑂 β†’ ((π‘β€˜dom 𝑂):(𝑏 Γ— 𝑏)–1-1-onto→𝑏 ↔ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-onto→𝑏))
41 f1oeq3 6823 . . . . . . . . . . . . 13 (𝑏 = dom 𝑂 β†’ ((π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-onto→𝑏 ↔ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’dom 𝑂))
4237, 40, 413bitrd 304 . . . . . . . . . . . 12 (𝑏 = dom 𝑂 β†’ ((π‘β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏 ↔ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’dom 𝑂))
4335, 42imbi12d 344 . . . . . . . . . . 11 (𝑏 = dom 𝑂 β†’ ((Ο‰ βŠ† 𝑏 β†’ (π‘β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏) ↔ (Ο‰ βŠ† dom 𝑂 β†’ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’dom 𝑂)))
44 pwfseqlem5.n . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘ ∈ (harβ€˜π’« 𝐴)(Ο‰ βŠ† 𝑏 β†’ (π‘β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏))
4544adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘ ∈ (harβ€˜π’« 𝐴)(Ο‰ βŠ† 𝑏 β†’ (π‘β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏))
4625a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ dom 𝑂 ∈ On)
471adantr 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ πœ“) β†’ 𝐺:𝒫 𝐴–1-1β†’βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛))
48 omex 9640 . . . . . . . . . . . . . . . . . 18 Ο‰ ∈ V
49 ovex 7444 . . . . . . . . . . . . . . . . . 18 (𝐴 ↑m 𝑛) ∈ V
5048, 49iunex 7957 . . . . . . . . . . . . . . . . 17 βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) ∈ V
51 f1dmex 7945 . . . . . . . . . . . . . . . . 17 ((𝐺:𝒫 𝐴–1-1β†’βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) ∧ βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) ∈ V) β†’ 𝒫 𝐴 ∈ V)
5247, 50, 51sylancl 586 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ πœ“) β†’ 𝒫 𝐴 ∈ V)
53 pwexb 7755 . . . . . . . . . . . . . . . 16 (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
5452, 53sylibr 233 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ 𝐴 ∈ V)
55 simprl1 1218 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ ((𝑑 βŠ† 𝐴 ∧ π‘Ÿ βŠ† (𝑑 Γ— 𝑑) ∧ π‘Ÿ We 𝑑) ∧ Ο‰ β‰Ό 𝑑)) β†’ 𝑑 βŠ† 𝐴)
564, 55sylan2b 594 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ 𝑑 βŠ† 𝐴)
57 ssdomg 8998 . . . . . . . . . . . . . . 15 (𝐴 ∈ V β†’ (𝑑 βŠ† 𝐴 β†’ 𝑑 β‰Ό 𝐴))
5854, 56, 57sylc 65 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ 𝑑 β‰Ό 𝐴)
59 canth2g 9133 . . . . . . . . . . . . . . 15 (𝐴 ∈ V β†’ 𝐴 β‰Ί 𝒫 𝐴)
60 sdomdom 8978 . . . . . . . . . . . . . . 15 (𝐴 β‰Ί 𝒫 𝐴 β†’ 𝐴 β‰Ό 𝒫 𝐴)
6154, 59, 603syl 18 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ 𝐴 β‰Ό 𝒫 𝐴)
62 domtr 9005 . . . . . . . . . . . . . 14 ((𝑑 β‰Ό 𝐴 ∧ 𝐴 β‰Ό 𝒫 𝐴) β†’ 𝑑 β‰Ό 𝒫 𝐴)
6358, 61, 62syl2anc 584 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ 𝑑 β‰Ό 𝒫 𝐴)
64 endomtr 9010 . . . . . . . . . . . . 13 ((dom 𝑂 β‰ˆ 𝑑 ∧ 𝑑 β‰Ό 𝒫 𝐴) β†’ dom 𝑂 β‰Ό 𝒫 𝐴)
6517, 63, 64syl2anc 584 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ dom 𝑂 β‰Ό 𝒫 𝐴)
66 elharval 9558 . . . . . . . . . . . 12 (dom 𝑂 ∈ (harβ€˜π’« 𝐴) ↔ (dom 𝑂 ∈ On ∧ dom 𝑂 β‰Ό 𝒫 𝐴))
6746, 65, 66sylanbrc 583 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ dom 𝑂 ∈ (harβ€˜π’« 𝐴))
6843, 45, 67rspcdva 3613 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ (Ο‰ βŠ† dom 𝑂 β†’ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’dom 𝑂))
6934, 68mpd 15 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’dom 𝑂)
70 f1oco 6856 . . . . . . . . 9 ((𝑂:dom 𝑂–1-1-onto→𝑑 ∧ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’dom 𝑂) β†’ (𝑂 ∘ (π‘β€˜dom 𝑂)):(dom 𝑂 Γ— dom 𝑂)–1-1-onto→𝑑)
7112, 69, 70syl2anc 584 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ (𝑂 ∘ (π‘β€˜dom 𝑂)):(dom 𝑂 Γ— dom 𝑂)–1-1-onto→𝑑)
72 f1of 6833 . . . . . . . . . . . . . . 15 (𝑂:dom 𝑂–1-1-onto→𝑑 β†’ 𝑂:dom π‘‚βŸΆπ‘‘)
7312, 72syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ 𝑂:dom π‘‚βŸΆπ‘‘)
7473feqmptd 6960 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ 𝑂 = (𝑒 ∈ dom 𝑂 ↦ (π‘‚β€˜π‘’)))
7574f1oeq1d 6828 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ (𝑂:dom 𝑂–1-1-onto→𝑑 ↔ (𝑒 ∈ dom 𝑂 ↦ (π‘‚β€˜π‘’)):dom 𝑂–1-1-onto→𝑑))
7612, 75mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ (𝑒 ∈ dom 𝑂 ↦ (π‘‚β€˜π‘’)):dom 𝑂–1-1-onto→𝑑)
7773feqmptd 6960 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ 𝑂 = (𝑣 ∈ dom 𝑂 ↦ (π‘‚β€˜π‘£)))
7877f1oeq1d 6828 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ (𝑂:dom 𝑂–1-1-onto→𝑑 ↔ (𝑣 ∈ dom 𝑂 ↦ (π‘‚β€˜π‘£)):dom 𝑂–1-1-onto→𝑑))
7912, 78mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ (𝑣 ∈ dom 𝑂 ↦ (π‘‚β€˜π‘£)):dom 𝑂–1-1-onto→𝑑)
8076, 79xpf1o 9141 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ (𝑒 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(π‘‚β€˜π‘’), (π‘‚β€˜π‘£)⟩):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’(𝑑 Γ— 𝑑))
81 pwfseqlem5.t . . . . . . . . . . 11 𝑇 = (𝑒 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(π‘‚β€˜π‘’), (π‘‚β€˜π‘£)⟩)
82 f1oeq1 6821 . . . . . . . . . . 11 (𝑇 = (𝑒 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(π‘‚β€˜π‘’), (π‘‚β€˜π‘£)⟩) β†’ (𝑇:(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’(𝑑 Γ— 𝑑) ↔ (𝑒 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(π‘‚β€˜π‘’), (π‘‚β€˜π‘£)⟩):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’(𝑑 Γ— 𝑑)))
8381, 82ax-mp 5 . . . . . . . . . 10 (𝑇:(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’(𝑑 Γ— 𝑑) ↔ (𝑒 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(π‘‚β€˜π‘’), (π‘‚β€˜π‘£)⟩):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’(𝑑 Γ— 𝑑))
8480, 83sylibr 233 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ 𝑇:(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’(𝑑 Γ— 𝑑))
85 f1ocnv 6845 . . . . . . . . 9 (𝑇:(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’(𝑑 Γ— 𝑑) β†’ ◑𝑇:(𝑑 Γ— 𝑑)–1-1-ontoβ†’(dom 𝑂 Γ— dom 𝑂))
8684, 85syl 17 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ ◑𝑇:(𝑑 Γ— 𝑑)–1-1-ontoβ†’(dom 𝑂 Γ— dom 𝑂))
87 f1oco 6856 . . . . . . . 8 (((𝑂 ∘ (π‘β€˜dom 𝑂)):(dom 𝑂 Γ— dom 𝑂)–1-1-onto→𝑑 ∧ ◑𝑇:(𝑑 Γ— 𝑑)–1-1-ontoβ†’(dom 𝑂 Γ— dom 𝑂)) β†’ ((𝑂 ∘ (π‘β€˜dom 𝑂)) ∘ ◑𝑇):(𝑑 Γ— 𝑑)–1-1-onto→𝑑)
8871, 86, 87syl2anc 584 . . . . . . 7 ((πœ‘ ∧ πœ“) β†’ ((𝑂 ∘ (π‘β€˜dom 𝑂)) ∘ ◑𝑇):(𝑑 Γ— 𝑑)–1-1-onto→𝑑)
89 pwfseqlem5.p . . . . . . . 8 𝑃 = ((𝑂 ∘ (π‘β€˜dom 𝑂)) ∘ ◑𝑇)
90 f1oeq1 6821 . . . . . . . 8 (𝑃 = ((𝑂 ∘ (π‘β€˜dom 𝑂)) ∘ ◑𝑇) β†’ (𝑃:(𝑑 Γ— 𝑑)–1-1-onto→𝑑 ↔ ((𝑂 ∘ (π‘β€˜dom 𝑂)) ∘ ◑𝑇):(𝑑 Γ— 𝑑)–1-1-onto→𝑑))
9189, 90ax-mp 5 . . . . . . 7 (𝑃:(𝑑 Γ— 𝑑)–1-1-onto→𝑑 ↔ ((𝑂 ∘ (π‘β€˜dom 𝑂)) ∘ ◑𝑇):(𝑑 Γ— 𝑑)–1-1-onto→𝑑)
9288, 91sylibr 233 . . . . . 6 ((πœ‘ ∧ πœ“) β†’ 𝑃:(𝑑 Γ— 𝑑)–1-1-onto→𝑑)
93 f1of1 6832 . . . . . 6 (𝑃:(𝑑 Γ— 𝑑)–1-1-onto→𝑑 β†’ 𝑃:(𝑑 Γ— 𝑑)–1-1→𝑑)
9492, 93syl 17 . . . . 5 ((πœ‘ ∧ πœ“) β†’ 𝑃:(𝑑 Γ— 𝑑)–1-1→𝑑)
95 f1of1 6832 . . . . . . . . . . . . 13 (𝑂:dom 𝑂–1-1-onto→𝑑 β†’ 𝑂:dom 𝑂–1-1→𝑑)
9612, 95syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ 𝑂:dom 𝑂–1-1→𝑑)
97 f1ssres 6795 . . . . . . . . . . . 12 ((𝑂:dom 𝑂–1-1→𝑑 ∧ Ο‰ βŠ† dom 𝑂) β†’ (𝑂 β†Ύ Ο‰):ω–1-1→𝑑)
9896, 34, 97syl2anc 584 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ (𝑂 β†Ύ Ο‰):ω–1-1→𝑑)
99 f1f1orn 6844 . . . . . . . . . . 11 ((𝑂 β†Ύ Ο‰):ω–1-1→𝑑 β†’ (𝑂 β†Ύ Ο‰):ω–1-1-ontoβ†’ran (𝑂 β†Ύ Ο‰))
10098, 99syl 17 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ (𝑂 β†Ύ Ο‰):ω–1-1-ontoβ†’ran (𝑂 β†Ύ Ο‰))
10173, 34feqresmpt 6961 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ (𝑂 β†Ύ Ο‰) = (π‘₯ ∈ Ο‰ ↦ (π‘‚β€˜π‘₯)))
102101f1oeq1d 6828 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ ((𝑂 β†Ύ Ο‰):ω–1-1-ontoβ†’ran (𝑂 β†Ύ Ο‰) ↔ (π‘₯ ∈ Ο‰ ↦ (π‘‚β€˜π‘₯)):ω–1-1-ontoβ†’ran (𝑂 β†Ύ Ο‰)))
103100, 102mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (π‘₯ ∈ Ο‰ ↦ (π‘‚β€˜π‘₯)):ω–1-1-ontoβ†’ran (𝑂 β†Ύ Ο‰))
104 mptresid 6050 . . . . . . . . . . 11 ( I β†Ύ 𝑑) = (𝑦 ∈ 𝑑 ↦ 𝑦)
105104eqcomi 2741 . . . . . . . . . 10 (𝑦 ∈ 𝑑 ↦ 𝑦) = ( I β†Ύ 𝑑)
106 f1oi 6871 . . . . . . . . . . 11 ( I β†Ύ 𝑑):𝑑–1-1-onto→𝑑
107 f1oeq1 6821 . . . . . . . . . . 11 ((𝑦 ∈ 𝑑 ↦ 𝑦) = ( I β†Ύ 𝑑) β†’ ((𝑦 ∈ 𝑑 ↦ 𝑦):𝑑–1-1-onto→𝑑 ↔ ( I β†Ύ 𝑑):𝑑–1-1-onto→𝑑))
108106, 107mpbiri 257 . . . . . . . . . 10 ((𝑦 ∈ 𝑑 ↦ 𝑦) = ( I β†Ύ 𝑑) β†’ (𝑦 ∈ 𝑑 ↦ 𝑦):𝑑–1-1-onto→𝑑)
109105, 108mp1i 13 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (𝑦 ∈ 𝑑 ↦ 𝑦):𝑑–1-1-onto→𝑑)
110103, 109xpf1o 9141 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ (π‘₯ ∈ Ο‰, 𝑦 ∈ 𝑑 ↦ ⟨(π‘‚β€˜π‘₯), π‘¦βŸ©):(Ο‰ Γ— 𝑑)–1-1-ontoβ†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑))
111 pwfseqlem5.i . . . . . . . . 9 𝐼 = (π‘₯ ∈ Ο‰, 𝑦 ∈ 𝑑 ↦ ⟨(π‘‚β€˜π‘₯), π‘¦βŸ©)
112 f1oeq1 6821 . . . . . . . . 9 (𝐼 = (π‘₯ ∈ Ο‰, 𝑦 ∈ 𝑑 ↦ ⟨(π‘‚β€˜π‘₯), π‘¦βŸ©) β†’ (𝐼:(Ο‰ Γ— 𝑑)–1-1-ontoβ†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑) ↔ (π‘₯ ∈ Ο‰, 𝑦 ∈ 𝑑 ↦ ⟨(π‘‚β€˜π‘₯), π‘¦βŸ©):(Ο‰ Γ— 𝑑)–1-1-ontoβ†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑)))
113111, 112ax-mp 5 . . . . . . . 8 (𝐼:(Ο‰ Γ— 𝑑)–1-1-ontoβ†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑) ↔ (π‘₯ ∈ Ο‰, 𝑦 ∈ 𝑑 ↦ ⟨(π‘‚β€˜π‘₯), π‘¦βŸ©):(Ο‰ Γ— 𝑑)–1-1-ontoβ†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑))
114110, 113sylibr 233 . . . . . . 7 ((πœ‘ ∧ πœ“) β†’ 𝐼:(Ο‰ Γ— 𝑑)–1-1-ontoβ†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑))
115 f1of1 6832 . . . . . . 7 (𝐼:(Ο‰ Γ— 𝑑)–1-1-ontoβ†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑) β†’ 𝐼:(Ο‰ Γ— 𝑑)–1-1β†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑))
116114, 115syl 17 . . . . . 6 ((πœ‘ ∧ πœ“) β†’ 𝐼:(Ο‰ Γ— 𝑑)–1-1β†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑))
117 f1f 6787 . . . . . . 7 ((𝑂 β†Ύ Ο‰):ω–1-1→𝑑 β†’ (𝑂 β†Ύ Ο‰):Ο‰βŸΆπ‘‘)
118 frn 6724 . . . . . . 7 ((𝑂 β†Ύ Ο‰):Ο‰βŸΆπ‘‘ β†’ ran (𝑂 β†Ύ Ο‰) βŠ† 𝑑)
119 xpss1 5695 . . . . . . 7 (ran (𝑂 β†Ύ Ο‰) βŠ† 𝑑 β†’ (ran (𝑂 β†Ύ Ο‰) Γ— 𝑑) βŠ† (𝑑 Γ— 𝑑))
12098, 117, 118, 1194syl 19 . . . . . 6 ((πœ‘ ∧ πœ“) β†’ (ran (𝑂 β†Ύ Ο‰) Γ— 𝑑) βŠ† (𝑑 Γ— 𝑑))
121 f1ss 6793 . . . . . 6 ((𝐼:(Ο‰ Γ— 𝑑)–1-1β†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑) ∧ (ran (𝑂 β†Ύ Ο‰) Γ— 𝑑) βŠ† (𝑑 Γ— 𝑑)) β†’ 𝐼:(Ο‰ Γ— 𝑑)–1-1β†’(𝑑 Γ— 𝑑))
122116, 120, 121syl2anc 584 . . . . 5 ((πœ‘ ∧ πœ“) β†’ 𝐼:(Ο‰ Γ— 𝑑)–1-1β†’(𝑑 Γ— 𝑑))
123 f1co 6799 . . . . 5 ((𝑃:(𝑑 Γ— 𝑑)–1-1→𝑑 ∧ 𝐼:(Ο‰ Γ— 𝑑)–1-1β†’(𝑑 Γ— 𝑑)) β†’ (𝑃 ∘ 𝐼):(Ο‰ Γ— 𝑑)–1-1→𝑑)
12494, 122, 123syl2anc 584 . . . 4 ((πœ‘ ∧ πœ“) β†’ (𝑃 ∘ 𝐼):(Ο‰ Γ— 𝑑)–1-1→𝑑)
1255a1i 11 . . . . 5 ((πœ‘ ∧ πœ“) β†’ 𝑑 ∈ V)
126 peano1 7881 . . . . . . . 8 βˆ… ∈ Ο‰
127126a1i 11 . . . . . . 7 ((πœ‘ ∧ πœ“) β†’ βˆ… ∈ Ο‰)
12834, 127sseldd 3983 . . . . . 6 ((πœ‘ ∧ πœ“) β†’ βˆ… ∈ dom 𝑂)
12973, 128ffvelcdmd 7087 . . . . 5 ((πœ‘ ∧ πœ“) β†’ (π‘‚β€˜βˆ…) ∈ 𝑑)
130 pwfseqlem5.s . . . . 5 𝑆 = seqΟ‰((π‘˜ ∈ V, 𝑓 ∈ V ↦ (π‘₯ ∈ (𝑑 ↑m suc π‘˜) ↦ ((π‘“β€˜(π‘₯ β†Ύ π‘˜))𝑃(π‘₯β€˜π‘˜)))), {βŸ¨βˆ…, (π‘‚β€˜βˆ…)⟩})
131 pwfseqlem5.q . . . . 5 𝑄 = (𝑦 ∈ βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛) ↦ ⟨dom 𝑦, ((π‘†β€˜dom 𝑦)β€˜π‘¦)⟩)
132125, 129, 92, 130, 131fseqenlem2 10022 . . . 4 ((πœ‘ ∧ πœ“) β†’ 𝑄:βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛)–1-1β†’(Ο‰ Γ— 𝑑))
133 f1co 6799 . . . 4 (((𝑃 ∘ 𝐼):(Ο‰ Γ— 𝑑)–1-1→𝑑 ∧ 𝑄:βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛)–1-1β†’(Ο‰ Γ— 𝑑)) β†’ ((𝑃 ∘ 𝐼) ∘ 𝑄):βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛)–1-1→𝑑)
134124, 132, 133syl2anc 584 . . 3 ((πœ‘ ∧ πœ“) β†’ ((𝑃 ∘ 𝐼) ∘ 𝑄):βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛)–1-1→𝑑)
135 pwfseqlem5.k . . . 4 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄)
136 f1eq1 6782 . . . 4 (𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) β†’ (𝐾:βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛)–1-1→𝑑 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛)–1-1→𝑑))
137135, 136ax-mp 5 . . 3 (𝐾:βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛)–1-1→𝑑 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛)–1-1→𝑑)
138134, 137sylibr 233 . 2 ((πœ‘ ∧ πœ“) β†’ 𝐾:βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛)–1-1→𝑑)
139 eqid 2732 . 2 (πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))}) = (πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})
140 eqid 2732 . 2 (𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑}))) = (𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑})))
141 eqid 2732 . . 3 {βŸ¨π‘, π‘‘βŸ© ∣ ((𝑐 βŠ† 𝐴 ∧ 𝑑 βŠ† (𝑐 Γ— 𝑐)) ∧ (𝑑 We 𝑐 ∧ βˆ€π‘š ∈ 𝑐 [(◑𝑑 β€œ {π‘š}) / 𝑗](𝑗(𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑})))(𝑑 ∩ (𝑗 Γ— 𝑗))) = π‘š))} = {βŸ¨π‘, π‘‘βŸ© ∣ ((𝑐 βŠ† 𝐴 ∧ 𝑑 βŠ† (𝑐 Γ— 𝑐)) ∧ (𝑑 We 𝑐 ∧ βˆ€π‘š ∈ 𝑐 [(◑𝑑 β€œ {π‘š}) / 𝑗](𝑗(𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑})))(𝑑 ∩ (𝑗 Γ— 𝑗))) = π‘š))}
142141fpwwe2cbv 10627 . 2 {βŸ¨π‘, π‘‘βŸ© ∣ ((𝑐 βŠ† 𝐴 ∧ 𝑑 βŠ† (𝑐 Γ— 𝑐)) ∧ (𝑑 We 𝑐 ∧ βˆ€π‘š ∈ 𝑐 [(◑𝑑 β€œ {π‘š}) / 𝑗](𝑗(𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑})))(𝑑 ∩ (𝑗 Γ— 𝑗))) = π‘š))} = {βŸ¨π‘Ž, π‘ βŸ© ∣ ((π‘Ž βŠ† 𝐴 ∧ 𝑠 βŠ† (π‘Ž Γ— π‘Ž)) ∧ (𝑠 We π‘Ž ∧ βˆ€π‘ ∈ π‘Ž [(◑𝑠 β€œ {𝑏}) / 𝑀](𝑀(𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑})))(𝑠 ∩ (𝑀 Γ— 𝑀))) = 𝑏))}
143 eqid 2732 . 2 βˆͺ dom {βŸ¨π‘, π‘‘βŸ© ∣ ((𝑐 βŠ† 𝐴 ∧ 𝑑 βŠ† (𝑐 Γ— 𝑐)) ∧ (𝑑 We 𝑐 ∧ βˆ€π‘š ∈ 𝑐 [(◑𝑑 β€œ {π‘š}) / 𝑗](𝑗(𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑})))(𝑑 ∩ (𝑗 Γ— 𝑗))) = π‘š))} = βˆͺ dom {βŸ¨π‘, π‘‘βŸ© ∣ ((𝑐 βŠ† 𝐴 ∧ 𝑑 βŠ† (𝑐 Γ— 𝑐)) ∧ (𝑑 We 𝑐 ∧ βˆ€π‘š ∈ 𝑐 [(◑𝑑 β€œ {π‘š}) / 𝑗](𝑗(𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑})))(𝑑 ∩ (𝑗 Γ— 𝑗))) = π‘š))}
1441, 2, 3, 4, 138, 139, 140, 142, 143pwfseqlem4 10659 1 Β¬ πœ‘
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  {crab 3432  Vcvv 3474  [wsbc 3777   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  ifcif 4528  π’« cpw 4602  {csn 4628  βŸ¨cop 4634  βˆͺ cuni 4908  βˆ© cint 4950  βˆͺ ciun 4997   class class class wbr 5148  {copab 5210   ↦ cmpt 5231   I cid 5573   E cep 5579   We wwe 5630   Γ— cxp 5674  β—‘ccnv 5675  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679   ∘ ccom 5680  Oncon0 6364  suc csuc 6366  βŸΆwf 6539  β€“1-1β†’wf1 6540  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543   Isom wiso 6544  (class class class)co 7411   ∈ cmpo 7413  Ο‰com 7857  seqΟ‰cseqom 8449   ↑m cmap 8822   β‰ˆ cen 8938   β‰Ό cdom 8939   β‰Ί csdm 8940  Fincfn 8941  OrdIsocoi 9506  harchar 9553  cardccrd 9932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-seqom 8450  df-1o 8468  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-oi 9507  df-har 9554  df-card 9936
This theorem is referenced by:  pwfseq  10661
  Copyright terms: Public domain W3C validator