Metamath Proof Explorer

Theorem pwfseqlem2

Description: Lemma for pwfseq . (Contributed by Mario Carneiro, 18-Nov-2014) (Revised by AV, 18-Sep-2021)

Ref Expression
Hypotheses pwfseqlem4.g ⊢φ→G:𝒫A⟶1-1⋃n∈ωAn
pwfseqlem4.x ⊢φ→X⊆A
pwfseqlem4.h ⊢φ→H:ω⟶1-1 ontoX
pwfseqlem4.ps ⊢ψ↔x⊆A∧r⊆x×x∧rWex∧ω≼x
pwfseqlem4.k ⊢φ∧ψ→K:⋃n∈ωxn⟶1-1x
pwfseqlem4.d ⊢D=G⁡w∈x|K-1⁡w∈ran⁡G∧¬w∈G-1⁡K-1⁡w
pwfseqlem4.f ⊢F=x∈V,r∈V⟼ifx∈FinH⁡card⁡xD⁡⋂z∈ω|¬D⁡z∈x
Assertion pwfseqlem2 ⊢Y∈Fin∧R∈V→YFR=H⁡card⁡Y

Proof

Step Hyp Ref Expression
1 pwfseqlem4.g ⊢φ→G:𝒫A⟶1-1⋃n∈ωAn
2 pwfseqlem4.x ⊢φ→X⊆A
3 pwfseqlem4.h ⊢φ→H:ω⟶1-1 ontoX
4 pwfseqlem4.ps ⊢ψ↔x⊆A∧r⊆x×x∧rWex∧ω≼x
5 pwfseqlem4.k ⊢φ∧ψ→K:⋃n∈ωxn⟶1-1x
6 pwfseqlem4.d ⊢D=G⁡w∈x|K-1⁡w∈ran⁡G∧¬w∈G-1⁡K-1⁡w
7 pwfseqlem4.f ⊢F=x∈V,r∈V⟼ifx∈FinH⁡card⁡xD⁡⋂z∈ω|¬D⁡z∈x
8 oveq1 ⊢a=Y→aFs=YFs
9 2fveq3 ⊢a=Y→H⁡card⁡a=H⁡card⁡Y
10 8 9 eqeq12d ⊢a=Y→aFs=H⁡card⁡a↔YFs=H⁡card⁡Y
11 oveq2 ⊢s=R→YFs=YFR
12 11 eqeq1d ⊢s=R→YFs=H⁡card⁡Y↔YFR=H⁡card⁡Y
13 nfcv ⊢Ⅎ_xa
14 nfcv ⊢Ⅎ_ra
15 nfcv ⊢Ⅎ_rs
16 nfmpo1 ⊢Ⅎ_xx∈V,r∈V⟼ifx∈FinH⁡card⁡xD⁡⋂z∈ω|¬D⁡z∈x
17 7 16 nfcxfr ⊢Ⅎ_xF
18 nfcv ⊢Ⅎ_xr
19 13 17 18 nfov ⊢Ⅎ_xaFr
20 19 nfeq1 ⊢ℲxaFr=H⁡card⁡a
21 nfmpo2 ⊢Ⅎ_rx∈V,r∈V⟼ifx∈FinH⁡card⁡xD⁡⋂z∈ω|¬D⁡z∈x
22 7 21 nfcxfr ⊢Ⅎ_rF
23 14 22 15 nfov ⊢Ⅎ_raFs
24 23 nfeq1 ⊢ℲraFs=H⁡card⁡a
25 oveq1 ⊢x=a→xFr=aFr
26 2fveq3 ⊢x=a→H⁡card⁡x=H⁡card⁡a
27 25 26 eqeq12d ⊢x=a→xFr=H⁡card⁡x↔aFr=H⁡card⁡a
28 oveq2 ⊢r=s→aFr=aFs
29 28 eqeq1d ⊢r=s→aFr=H⁡card⁡a↔aFs=H⁡card⁡a
30 vex ⊢x∈V
31 vex ⊢r∈V
32 fvex ⊢H⁡card⁡x∈V
33 fvex ⊢D⁡⋂z∈ω|¬D⁡z∈x∈V
34 32 33 ifex ⊢ifx∈FinH⁡card⁡xD⁡⋂z∈ω|¬D⁡z∈x∈V
35 7 ovmpt4g ⊢x∈V∧r∈V∧ifx∈FinH⁡card⁡xD⁡⋂z∈ω|¬D⁡z∈x∈V→xFr=ifx∈FinH⁡card⁡xD⁡⋂z∈ω|¬D⁡z∈x
36 30 31 34 35 mp3an ⊢xFr=ifx∈FinH⁡card⁡xD⁡⋂z∈ω|¬D⁡z∈x
37 iftrue ⊢x∈Fin→ifx∈FinH⁡card⁡xD⁡⋂z∈ω|¬D⁡z∈x=H⁡card⁡x
38 36 37 eqtrid ⊢x∈Fin→xFr=H⁡card⁡x
39 38 adantr ⊢x∈Fin∧r∈V→xFr=H⁡card⁡x
40 13 14 15 20 24 27 29 39 vtocl2gaf ⊢a∈Fin∧s∈V→aFs=H⁡card⁡a
41 10 12 40 vtocl2ga ⊢Y∈Fin∧R∈V→YFR=H⁡card⁡Y