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

Theorem pwfseqlem5 10658
Description: Lemma for pwfseq 10659. Although in some ways pwfseqlem4 10657 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 10022. 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 10009. 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 9701), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 10013). (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 3479 . . . . . . . . . . 11 𝑑 ∈ V
6 simprl3 1221 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑑 βŠ† 𝐴 ∧ π‘Ÿ βŠ† (𝑑 Γ— 𝑑) ∧ π‘Ÿ We 𝑑) ∧ Ο‰ β‰Ό 𝑑)) β†’ π‘Ÿ We 𝑑)
74, 6sylan2b 595 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ π‘Ÿ We 𝑑)
8 pwfseqlem5.o . . . . . . . . . . . 12 𝑂 = OrdIso(π‘Ÿ, 𝑑)
98oiiso 9532 . . . . . . . . . . 11 ((𝑑 ∈ V ∧ π‘Ÿ We 𝑑) β†’ 𝑂 Isom E , π‘Ÿ (dom 𝑂, 𝑑))
105, 7, 9sylancr 588 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ 𝑂 Isom E , π‘Ÿ (dom 𝑂, 𝑑))
11 isof1o 7320 . . . . . . . . . 10 (𝑂 Isom E , π‘Ÿ (dom 𝑂, 𝑑) β†’ 𝑂:dom 𝑂–1-1-onto→𝑑)
1210, 11syl 17 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ 𝑂:dom 𝑂–1-1-onto→𝑑)
13 cardom 9981 . . . . . . . . . . . 12 (cardβ€˜Ο‰) = Ο‰
14 simprr 772 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ ((𝑑 βŠ† 𝐴 ∧ π‘Ÿ βŠ† (𝑑 Γ— 𝑑) ∧ π‘Ÿ We 𝑑) ∧ Ο‰ β‰Ό 𝑑)) β†’ Ο‰ β‰Ό 𝑑)
154, 14sylan2b 595 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ Ο‰ β‰Ό 𝑑)
168oien 9533 . . . . . . . . . . . . . . . 16 ((𝑑 ∈ V ∧ π‘Ÿ We 𝑑) β†’ dom 𝑂 β‰ˆ 𝑑)
175, 7, 16sylancr 588 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ dom 𝑂 β‰ˆ 𝑑)
1817ensymd 9001 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ 𝑑 β‰ˆ dom 𝑂)
19 domentr 9009 . . . . . . . . . . . . . 14 ((Ο‰ β‰Ό 𝑑 ∧ 𝑑 β‰ˆ dom 𝑂) β†’ Ο‰ β‰Ό dom 𝑂)
2015, 18, 19syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ Ο‰ β‰Ό dom 𝑂)
21 omelon 9641 . . . . . . . . . . . . . . 15 Ο‰ ∈ On
22 onenon 9944 . . . . . . . . . . . . . . 15 (Ο‰ ∈ On β†’ Ο‰ ∈ dom card)
2321, 22ax-mp 5 . . . . . . . . . . . . . 14 Ο‰ ∈ dom card
248oion 9531 . . . . . . . . . . . . . . . 16 (𝑑 ∈ V β†’ dom 𝑂 ∈ On)
2524elv 3481 . . . . . . . . . . . . . . 15 dom 𝑂 ∈ On
26 onenon 9944 . . . . . . . . . . . . . . 15 (dom 𝑂 ∈ On β†’ dom 𝑂 ∈ dom card)
2725, 26mp1i 13 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ dom 𝑂 ∈ dom card)
28 carddom2 9972 . . . . . . . . . . . . . 14 ((Ο‰ ∈ dom card ∧ dom 𝑂 ∈ dom card) β†’ ((cardβ€˜Ο‰) βŠ† (cardβ€˜dom 𝑂) ↔ Ο‰ β‰Ό dom 𝑂))
2923, 27, 28sylancr 588 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ ((cardβ€˜Ο‰) βŠ† (cardβ€˜dom 𝑂) ↔ Ο‰ β‰Ό dom 𝑂))
3020, 29mpbird 257 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ (cardβ€˜Ο‰) βŠ† (cardβ€˜dom 𝑂))
3113, 30eqsstrrid 4032 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ Ο‰ βŠ† (cardβ€˜dom 𝑂))
32 cardonle 9952 . . . . . . . . . . . 12 (dom 𝑂 ∈ On β†’ (cardβ€˜dom 𝑂) βŠ† dom 𝑂)
3325, 32mp1i 13 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ (cardβ€˜dom 𝑂) βŠ† dom 𝑂)
3431, 33sstrd 3993 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ Ο‰ βŠ† dom 𝑂)
35 sseq2 4009 . . . . . . . . . . . 12 (𝑏 = dom 𝑂 β†’ (Ο‰ βŠ† 𝑏 ↔ Ο‰ βŠ† dom 𝑂))
36 fveq2 6892 . . . . . . . . . . . . . 14 (𝑏 = dom 𝑂 β†’ (π‘β€˜π‘) = (π‘β€˜dom 𝑂))
3736f1oeq1d 6829 . . . . . . . . . . . . 13 (𝑏 = dom 𝑂 β†’ ((π‘β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏 ↔ (π‘β€˜dom 𝑂):(𝑏 Γ— 𝑏)–1-1-onto→𝑏))
38 xpeq12 5702 . . . . . . . . . . . . . . 15 ((𝑏 = dom 𝑂 ∧ 𝑏 = dom 𝑂) β†’ (𝑏 Γ— 𝑏) = (dom 𝑂 Γ— dom 𝑂))
3938anidms 568 . . . . . . . . . . . . . 14 (𝑏 = dom 𝑂 β†’ (𝑏 Γ— 𝑏) = (dom 𝑂 Γ— dom 𝑂))
4039f1oeq2d 6830 . . . . . . . . . . . . 13 (𝑏 = dom 𝑂 β†’ ((π‘β€˜dom 𝑂):(𝑏 Γ— 𝑏)–1-1-onto→𝑏 ↔ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-onto→𝑏))
41 f1oeq3 6824 . . . . . . . . . . . . 13 (𝑏 = dom 𝑂 β†’ ((π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-onto→𝑏 ↔ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’dom 𝑂))
4237, 40, 413bitrd 305 . . . . . . . . . . . 12 (𝑏 = dom 𝑂 β†’ ((π‘β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏 ↔ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’dom 𝑂))
4335, 42imbi12d 345 . . . . . . . . . . 11 (𝑏 = dom 𝑂 β†’ ((Ο‰ βŠ† 𝑏 β†’ (π‘β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏) ↔ (Ο‰ βŠ† dom 𝑂 β†’ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’dom 𝑂)))
44 pwfseqlem5.n . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘ ∈ (harβ€˜π’« 𝐴)(Ο‰ βŠ† 𝑏 β†’ (π‘β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏))
4544adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘ ∈ (harβ€˜π’« 𝐴)(Ο‰ βŠ† 𝑏 β†’ (π‘β€˜π‘):(𝑏 Γ— 𝑏)–1-1-onto→𝑏))
4625a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ dom 𝑂 ∈ On)
471adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ πœ“) β†’ 𝐺:𝒫 𝐴–1-1β†’βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛))
48 omex 9638 . . . . . . . . . . . . . . . . . 18 Ο‰ ∈ V
49 ovex 7442 . . . . . . . . . . . . . . . . . 18 (𝐴 ↑m 𝑛) ∈ V
5048, 49iunex 7955 . . . . . . . . . . . . . . . . 17 βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) ∈ V
51 f1dmex 7943 . . . . . . . . . . . . . . . . 17 ((𝐺:𝒫 𝐴–1-1β†’βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) ∧ βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) ∈ V) β†’ 𝒫 𝐴 ∈ V)
5247, 50, 51sylancl 587 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ πœ“) β†’ 𝒫 𝐴 ∈ V)
53 pwexb 7753 . . . . . . . . . . . . . . . 16 (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
5452, 53sylibr 233 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ 𝐴 ∈ V)
55 simprl1 1219 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ ((𝑑 βŠ† 𝐴 ∧ π‘Ÿ βŠ† (𝑑 Γ— 𝑑) ∧ π‘Ÿ We 𝑑) ∧ Ο‰ β‰Ό 𝑑)) β†’ 𝑑 βŠ† 𝐴)
564, 55sylan2b 595 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ 𝑑 βŠ† 𝐴)
57 ssdomg 8996 . . . . . . . . . . . . . . 15 (𝐴 ∈ V β†’ (𝑑 βŠ† 𝐴 β†’ 𝑑 β‰Ό 𝐴))
5854, 56, 57sylc 65 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ 𝑑 β‰Ό 𝐴)
59 canth2g 9131 . . . . . . . . . . . . . . 15 (𝐴 ∈ V β†’ 𝐴 β‰Ί 𝒫 𝐴)
60 sdomdom 8976 . . . . . . . . . . . . . . 15 (𝐴 β‰Ί 𝒫 𝐴 β†’ 𝐴 β‰Ό 𝒫 𝐴)
6154, 59, 603syl 18 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ 𝐴 β‰Ό 𝒫 𝐴)
62 domtr 9003 . . . . . . . . . . . . . 14 ((𝑑 β‰Ό 𝐴 ∧ 𝐴 β‰Ό 𝒫 𝐴) β†’ 𝑑 β‰Ό 𝒫 𝐴)
6358, 61, 62syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ 𝑑 β‰Ό 𝒫 𝐴)
64 endomtr 9008 . . . . . . . . . . . . 13 ((dom 𝑂 β‰ˆ 𝑑 ∧ 𝑑 β‰Ό 𝒫 𝐴) β†’ dom 𝑂 β‰Ό 𝒫 𝐴)
6517, 63, 64syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ dom 𝑂 β‰Ό 𝒫 𝐴)
66 elharval 9556 . . . . . . . . . . . 12 (dom 𝑂 ∈ (harβ€˜π’« 𝐴) ↔ (dom 𝑂 ∈ On ∧ dom 𝑂 β‰Ό 𝒫 𝐴))
6746, 65, 66sylanbrc 584 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ dom 𝑂 ∈ (harβ€˜π’« 𝐴))
6843, 45, 67rspcdva 3614 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ (Ο‰ βŠ† dom 𝑂 β†’ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’dom 𝑂))
6934, 68mpd 15 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’dom 𝑂)
70 f1oco 6857 . . . . . . . . 9 ((𝑂:dom 𝑂–1-1-onto→𝑑 ∧ (π‘β€˜dom 𝑂):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’dom 𝑂) β†’ (𝑂 ∘ (π‘β€˜dom 𝑂)):(dom 𝑂 Γ— dom 𝑂)–1-1-onto→𝑑)
7112, 69, 70syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ (𝑂 ∘ (π‘β€˜dom 𝑂)):(dom 𝑂 Γ— dom 𝑂)–1-1-onto→𝑑)
72 f1of 6834 . . . . . . . . . . . . . . 15 (𝑂:dom 𝑂–1-1-onto→𝑑 β†’ 𝑂:dom π‘‚βŸΆπ‘‘)
7312, 72syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ 𝑂:dom π‘‚βŸΆπ‘‘)
7473feqmptd 6961 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ 𝑂 = (𝑒 ∈ dom 𝑂 ↦ (π‘‚β€˜π‘’)))
7574f1oeq1d 6829 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ (𝑂:dom 𝑂–1-1-onto→𝑑 ↔ (𝑒 ∈ dom 𝑂 ↦ (π‘‚β€˜π‘’)):dom 𝑂–1-1-onto→𝑑))
7612, 75mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ (𝑒 ∈ dom 𝑂 ↦ (π‘‚β€˜π‘’)):dom 𝑂–1-1-onto→𝑑)
7773feqmptd 6961 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ 𝑂 = (𝑣 ∈ dom 𝑂 ↦ (π‘‚β€˜π‘£)))
7877f1oeq1d 6829 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ (𝑂:dom 𝑂–1-1-onto→𝑑 ↔ (𝑣 ∈ dom 𝑂 ↦ (π‘‚β€˜π‘£)):dom 𝑂–1-1-onto→𝑑))
7912, 78mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ (𝑣 ∈ dom 𝑂 ↦ (π‘‚β€˜π‘£)):dom 𝑂–1-1-onto→𝑑)
8076, 79xpf1o 9139 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ (𝑒 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(π‘‚β€˜π‘’), (π‘‚β€˜π‘£)⟩):(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’(𝑑 Γ— 𝑑))
81 pwfseqlem5.t . . . . . . . . . . 11 𝑇 = (𝑒 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(π‘‚β€˜π‘’), (π‘‚β€˜π‘£)⟩)
82 f1oeq1 6822 . . . . . . . . . . 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 6846 . . . . . . . . 9 (𝑇:(dom 𝑂 Γ— dom 𝑂)–1-1-ontoβ†’(𝑑 Γ— 𝑑) β†’ ◑𝑇:(𝑑 Γ— 𝑑)–1-1-ontoβ†’(dom 𝑂 Γ— dom 𝑂))
8684, 85syl 17 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ ◑𝑇:(𝑑 Γ— 𝑑)–1-1-ontoβ†’(dom 𝑂 Γ— dom 𝑂))
87 f1oco 6857 . . . . . . . 8 (((𝑂 ∘ (π‘β€˜dom 𝑂)):(dom 𝑂 Γ— dom 𝑂)–1-1-onto→𝑑 ∧ ◑𝑇:(𝑑 Γ— 𝑑)–1-1-ontoβ†’(dom 𝑂 Γ— dom 𝑂)) β†’ ((𝑂 ∘ (π‘β€˜dom 𝑂)) ∘ ◑𝑇):(𝑑 Γ— 𝑑)–1-1-onto→𝑑)
8871, 86, 87syl2anc 585 . . . . . . 7 ((πœ‘ ∧ πœ“) β†’ ((𝑂 ∘ (π‘β€˜dom 𝑂)) ∘ ◑𝑇):(𝑑 Γ— 𝑑)–1-1-onto→𝑑)
89 pwfseqlem5.p . . . . . . . 8 𝑃 = ((𝑂 ∘ (π‘β€˜dom 𝑂)) ∘ ◑𝑇)
90 f1oeq1 6822 . . . . . . . 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 6833 . . . . . 6 (𝑃:(𝑑 Γ— 𝑑)–1-1-onto→𝑑 β†’ 𝑃:(𝑑 Γ— 𝑑)–1-1→𝑑)
9492, 93syl 17 . . . . 5 ((πœ‘ ∧ πœ“) β†’ 𝑃:(𝑑 Γ— 𝑑)–1-1→𝑑)
95 f1of1 6833 . . . . . . . . . . . . 13 (𝑂:dom 𝑂–1-1-onto→𝑑 β†’ 𝑂:dom 𝑂–1-1→𝑑)
9612, 95syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ 𝑂:dom 𝑂–1-1→𝑑)
97 f1ssres 6796 . . . . . . . . . . . 12 ((𝑂:dom 𝑂–1-1→𝑑 ∧ Ο‰ βŠ† dom 𝑂) β†’ (𝑂 β†Ύ Ο‰):ω–1-1→𝑑)
9896, 34, 97syl2anc 585 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ (𝑂 β†Ύ Ο‰):ω–1-1→𝑑)
99 f1f1orn 6845 . . . . . . . . . . 11 ((𝑂 β†Ύ Ο‰):ω–1-1→𝑑 β†’ (𝑂 β†Ύ Ο‰):ω–1-1-ontoβ†’ran (𝑂 β†Ύ Ο‰))
10098, 99syl 17 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ (𝑂 β†Ύ Ο‰):ω–1-1-ontoβ†’ran (𝑂 β†Ύ Ο‰))
10173, 34feqresmpt 6962 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ (𝑂 β†Ύ Ο‰) = (π‘₯ ∈ Ο‰ ↦ (π‘‚β€˜π‘₯)))
102101f1oeq1d 6829 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ ((𝑂 β†Ύ Ο‰):ω–1-1-ontoβ†’ran (𝑂 β†Ύ Ο‰) ↔ (π‘₯ ∈ Ο‰ ↦ (π‘‚β€˜π‘₯)):ω–1-1-ontoβ†’ran (𝑂 β†Ύ Ο‰)))
103100, 102mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (π‘₯ ∈ Ο‰ ↦ (π‘‚β€˜π‘₯)):ω–1-1-ontoβ†’ran (𝑂 β†Ύ Ο‰))
104 mptresid 6051 . . . . . . . . . . 11 ( I β†Ύ 𝑑) = (𝑦 ∈ 𝑑 ↦ 𝑦)
105104eqcomi 2742 . . . . . . . . . 10 (𝑦 ∈ 𝑑 ↦ 𝑦) = ( I β†Ύ 𝑑)
106 f1oi 6872 . . . . . . . . . . 11 ( I β†Ύ 𝑑):𝑑–1-1-onto→𝑑
107 f1oeq1 6822 . . . . . . . . . . 11 ((𝑦 ∈ 𝑑 ↦ 𝑦) = ( I β†Ύ 𝑑) β†’ ((𝑦 ∈ 𝑑 ↦ 𝑦):𝑑–1-1-onto→𝑑 ↔ ( I β†Ύ 𝑑):𝑑–1-1-onto→𝑑))
108106, 107mpbiri 258 . . . . . . . . . 10 ((𝑦 ∈ 𝑑 ↦ 𝑦) = ( I β†Ύ 𝑑) β†’ (𝑦 ∈ 𝑑 ↦ 𝑦):𝑑–1-1-onto→𝑑)
109105, 108mp1i 13 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (𝑦 ∈ 𝑑 ↦ 𝑦):𝑑–1-1-onto→𝑑)
110103, 109xpf1o 9139 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ (π‘₯ ∈ Ο‰, 𝑦 ∈ 𝑑 ↦ ⟨(π‘‚β€˜π‘₯), π‘¦βŸ©):(Ο‰ Γ— 𝑑)–1-1-ontoβ†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑))
111 pwfseqlem5.i . . . . . . . . 9 𝐼 = (π‘₯ ∈ Ο‰, 𝑦 ∈ 𝑑 ↦ ⟨(π‘‚β€˜π‘₯), π‘¦βŸ©)
112 f1oeq1 6822 . . . . . . . . 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 6833 . . . . . . 7 (𝐼:(Ο‰ Γ— 𝑑)–1-1-ontoβ†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑) β†’ 𝐼:(Ο‰ Γ— 𝑑)–1-1β†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑))
116114, 115syl 17 . . . . . 6 ((πœ‘ ∧ πœ“) β†’ 𝐼:(Ο‰ Γ— 𝑑)–1-1β†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑))
117 f1f 6788 . . . . . . 7 ((𝑂 β†Ύ Ο‰):ω–1-1→𝑑 β†’ (𝑂 β†Ύ Ο‰):Ο‰βŸΆπ‘‘)
118 frn 6725 . . . . . . 7 ((𝑂 β†Ύ Ο‰):Ο‰βŸΆπ‘‘ β†’ ran (𝑂 β†Ύ Ο‰) βŠ† 𝑑)
119 xpss1 5696 . . . . . . 7 (ran (𝑂 β†Ύ Ο‰) βŠ† 𝑑 β†’ (ran (𝑂 β†Ύ Ο‰) Γ— 𝑑) βŠ† (𝑑 Γ— 𝑑))
12098, 117, 118, 1194syl 19 . . . . . 6 ((πœ‘ ∧ πœ“) β†’ (ran (𝑂 β†Ύ Ο‰) Γ— 𝑑) βŠ† (𝑑 Γ— 𝑑))
121 f1ss 6794 . . . . . 6 ((𝐼:(Ο‰ Γ— 𝑑)–1-1β†’(ran (𝑂 β†Ύ Ο‰) Γ— 𝑑) ∧ (ran (𝑂 β†Ύ Ο‰) Γ— 𝑑) βŠ† (𝑑 Γ— 𝑑)) β†’ 𝐼:(Ο‰ Γ— 𝑑)–1-1β†’(𝑑 Γ— 𝑑))
122116, 120, 121syl2anc 585 . . . . 5 ((πœ‘ ∧ πœ“) β†’ 𝐼:(Ο‰ Γ— 𝑑)–1-1β†’(𝑑 Γ— 𝑑))
123 f1co 6800 . . . . 5 ((𝑃:(𝑑 Γ— 𝑑)–1-1→𝑑 ∧ 𝐼:(Ο‰ Γ— 𝑑)–1-1β†’(𝑑 Γ— 𝑑)) β†’ (𝑃 ∘ 𝐼):(Ο‰ Γ— 𝑑)–1-1→𝑑)
12494, 122, 123syl2anc 585 . . . 4 ((πœ‘ ∧ πœ“) β†’ (𝑃 ∘ 𝐼):(Ο‰ Γ— 𝑑)–1-1→𝑑)
1255a1i 11 . . . . 5 ((πœ‘ ∧ πœ“) β†’ 𝑑 ∈ V)
126 peano1 7879 . . . . . . . 8 βˆ… ∈ Ο‰
127126a1i 11 . . . . . . 7 ((πœ‘ ∧ πœ“) β†’ βˆ… ∈ Ο‰)
12834, 127sseldd 3984 . . . . . 6 ((πœ‘ ∧ πœ“) β†’ βˆ… ∈ dom 𝑂)
12973, 128ffvelcdmd 7088 . . . . 5 ((πœ‘ ∧ πœ“) β†’ (π‘‚β€˜βˆ…) ∈ 𝑑)
130 pwfseqlem5.s . . . . 5 𝑆 = seqΟ‰((π‘˜ ∈ V, 𝑓 ∈ V ↦ (π‘₯ ∈ (𝑑 ↑m suc π‘˜) ↦ ((π‘“β€˜(π‘₯ β†Ύ π‘˜))𝑃(π‘₯β€˜π‘˜)))), {βŸ¨βˆ…, (π‘‚β€˜βˆ…)⟩})
131 pwfseqlem5.q . . . . 5 𝑄 = (𝑦 ∈ βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛) ↦ ⟨dom 𝑦, ((π‘†β€˜dom 𝑦)β€˜π‘¦)⟩)
132125, 129, 92, 130, 131fseqenlem2 10020 . . . 4 ((πœ‘ ∧ πœ“) β†’ 𝑄:βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛)–1-1β†’(Ο‰ Γ— 𝑑))
133 f1co 6800 . . . 4 (((𝑃 ∘ 𝐼):(Ο‰ Γ— 𝑑)–1-1→𝑑 ∧ 𝑄:βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛)–1-1β†’(Ο‰ Γ— 𝑑)) β†’ ((𝑃 ∘ 𝐼) ∘ 𝑄):βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛)–1-1→𝑑)
134124, 132, 133syl2anc 585 . . 3 ((πœ‘ ∧ πœ“) β†’ ((𝑃 ∘ 𝐼) ∘ 𝑄):βˆͺ 𝑛 ∈ Ο‰ (𝑑 ↑m 𝑛)–1-1→𝑑)
135 pwfseqlem5.k . . . 4 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄)
136 f1eq1 6783 . . . 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 2733 . 2 (πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))}) = (πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})
140 eqid 2733 . 2 (𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑}))) = (𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑})))
141 eqid 2733 . . 3 {βŸ¨π‘, π‘‘βŸ© ∣ ((𝑐 βŠ† 𝐴 ∧ 𝑑 βŠ† (𝑐 Γ— 𝑐)) ∧ (𝑑 We 𝑐 ∧ βˆ€π‘š ∈ 𝑐 [(◑𝑑 β€œ {π‘š}) / 𝑗](𝑗(𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑})))(𝑑 ∩ (𝑗 Γ— 𝑗))) = π‘š))} = {βŸ¨π‘, π‘‘βŸ© ∣ ((𝑐 βŠ† 𝐴 ∧ 𝑑 βŠ† (𝑐 Γ— 𝑐)) ∧ (𝑑 We 𝑐 ∧ βˆ€π‘š ∈ 𝑐 [(◑𝑑 β€œ {π‘š}) / 𝑗](𝑗(𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑})))(𝑑 ∩ (𝑗 Γ— 𝑗))) = π‘š))}
142141fpwwe2cbv 10625 . 2 {βŸ¨π‘, π‘‘βŸ© ∣ ((𝑐 βŠ† 𝐴 ∧ 𝑑 βŠ† (𝑐 Γ— 𝑐)) ∧ (𝑑 We 𝑐 ∧ βˆ€π‘š ∈ 𝑐 [(◑𝑑 β€œ {π‘š}) / 𝑗](𝑗(𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑})))(𝑑 ∩ (𝑗 Γ— 𝑗))) = π‘š))} = {βŸ¨π‘Ž, π‘ βŸ© ∣ ((π‘Ž βŠ† 𝐴 ∧ 𝑠 βŠ† (π‘Ž Γ— π‘Ž)) ∧ (𝑠 We π‘Ž ∧ βˆ€π‘ ∈ π‘Ž [(◑𝑠 β€œ {𝑏}) / 𝑀](𝑀(𝑑 ∈ V, π‘Ÿ ∈ V ↦ if(𝑑 ∈ Fin, (π»β€˜(cardβ€˜π‘‘)), ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ ((πΊβ€˜{𝑖 ∈ 𝑑 ∣ ((β—‘πΎβ€˜π‘–) ∈ ran 𝐺 ∧ Β¬ 𝑖 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘–)))})β€˜π‘§) ∈ 𝑑})))(𝑠 ∩ (𝑀 Γ— 𝑀))) = 𝑏))}
143 eqid 2733 . 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 10657 1 Β¬ πœ‘
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  {crab 3433  Vcvv 3475  [wsbc 3778   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  ifcif 4529  π’« cpw 4603  {csn 4629  βŸ¨cop 4635  βˆͺ cuni 4909  βˆ© cint 4951  βˆͺ ciun 4998   class class class wbr 5149  {copab 5211   ↦ cmpt 5232   I cid 5574   E cep 5580   We wwe 5631   Γ— cxp 5675  β—‘ccnv 5676  dom cdm 5677  ran crn 5678   β†Ύ cres 5679   β€œ cima 5680   ∘ ccom 5681  Oncon0 6365  suc csuc 6367  βŸΆwf 6540  β€“1-1β†’wf1 6541  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544   Isom wiso 6545  (class class class)co 7409   ∈ cmpo 7411  Ο‰com 7855  seqΟ‰cseqom 8447   ↑m cmap 8820   β‰ˆ cen 8936   β‰Ό cdom 8937   β‰Ί csdm 8938  Fincfn 8939  OrdIsocoi 9504  harchar 9551  cardccrd 9930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-seqom 8448  df-1o 8466  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-oi 9505  df-har 9552  df-card 9934
This theorem is referenced by:  pwfseq  10659
  Copyright terms: Public domain W3C validator