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 ⊢ ( 𝜑 → 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
pwfseqlem4.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝐴 )
pwfseqlem4.h ⊢ ( 𝜑 → 𝐻 : ω –1-1-onto→ 𝑋 )
pwfseqlem4.ps ⊢ ( 𝜓 ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ∧ ω ≼ 𝑥 ) )
pwfseqlem4.k ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) –1-1→ 𝑥 )
pwfseqlem4.d ⊢ 𝐷 = ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } )
pwfseqlem4.f ⊢ 𝐹 = ( 𝑥 ∈ V , 𝑟 ∈ V ↦ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
Assertion pwfseqlem2 ( ( 𝑌 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑌 𝐹 𝑅 ) = ( 𝐻 ‘ ( card ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 pwfseqlem4.g ⊢ ( 𝜑 → 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
2 pwfseqlem4.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝐴 )
3 pwfseqlem4.h ⊢ ( 𝜑 → 𝐻 : ω –1-1-onto→ 𝑋 )
4 pwfseqlem4.ps ⊢ ( 𝜓 ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ∧ ω ≼ 𝑥 ) )
5 pwfseqlem4.k ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑m 𝑛 ) –1-1→ 𝑥 )
6 pwfseqlem4.d ⊢ 𝐷 = ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑤 ) ) ) } )
7 pwfseqlem4.f ⊢ 𝐹 = ( 𝑥 ∈ V , 𝑟 ∈ V ↦ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
8 oveq1 ⊢ ( 𝑎 = 𝑌 → ( 𝑎 𝐹 𝑠 ) = ( 𝑌 𝐹 𝑠 ) )
9 2fveq3 ⊢ ( 𝑎 = 𝑌 → ( 𝐻 ‘ ( card ‘ 𝑎 ) ) = ( 𝐻 ‘ ( card ‘ 𝑌 ) ) )
10 8 9 eqeq12d ⊢ ( 𝑎 = 𝑌 → ( ( 𝑎 𝐹 𝑠 ) = ( 𝐻 ‘ ( card ‘ 𝑎 ) ) ↔ ( 𝑌 𝐹 𝑠 ) = ( 𝐻 ‘ ( card ‘ 𝑌 ) ) ) )
11 oveq2 ⊢ ( 𝑠 = 𝑅 → ( 𝑌 𝐹 𝑠 ) = ( 𝑌 𝐹 𝑅 ) )
12 11 eqeq1d ⊢ ( 𝑠 = 𝑅 → ( ( 𝑌 𝐹 𝑠 ) = ( 𝐻 ‘ ( card ‘ 𝑌 ) ) ↔ ( 𝑌 𝐹 𝑅 ) = ( 𝐻 ‘ ( card ‘ 𝑌 ) ) ) )
13 nfcv ⊢ Ⅎ 𝑥 𝑎
14 nfcv ⊢ Ⅎ 𝑟 𝑎
15 nfcv ⊢ Ⅎ 𝑟 𝑠
16 nfmpo1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ V , 𝑟 ∈ V ↦ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
17 7 16 nfcxfr ⊢ Ⅎ 𝑥 𝐹
18 nfcv ⊢ Ⅎ 𝑥 𝑟
19 13 17 18 nfov ⊢ Ⅎ 𝑥 ( 𝑎 𝐹 𝑟 )
20 19 nfeq1 ⊢ Ⅎ 𝑥 ( 𝑎 𝐹 𝑟 ) = ( 𝐻 ‘ ( card ‘ 𝑎 ) )
21 nfmpo2 ⊢ Ⅎ 𝑟 ( 𝑥 ∈ V , 𝑟 ∈ V ↦ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
22 7 21 nfcxfr ⊢ Ⅎ 𝑟 𝐹
23 14 22 15 nfov ⊢ Ⅎ 𝑟 ( 𝑎 𝐹 𝑠 )
24 23 nfeq1 ⊢ Ⅎ 𝑟 ( 𝑎 𝐹 𝑠 ) = ( 𝐻 ‘ ( card ‘ 𝑎 ) )
25 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 𝐹 𝑟 ) = ( 𝑎 𝐹 𝑟 ) )
26 2fveq3 ⊢ ( 𝑥 = 𝑎 → ( 𝐻 ‘ ( card ‘ 𝑥 ) ) = ( 𝐻 ‘ ( card ‘ 𝑎 ) ) )
27 25 26 eqeq12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 𝐹 𝑟 ) = ( 𝐻 ‘ ( card ‘ 𝑥 ) ) ↔ ( 𝑎 𝐹 𝑟 ) = ( 𝐻 ‘ ( card ‘ 𝑎 ) ) ) )
28 oveq2 ⊢ ( 𝑟 = 𝑠 → ( 𝑎 𝐹 𝑟 ) = ( 𝑎 𝐹 𝑠 ) )
29 28 eqeq1d ⊢ ( 𝑟 = 𝑠 → ( ( 𝑎 𝐹 𝑟 ) = ( 𝐻 ‘ ( card ‘ 𝑎 ) ) ↔ ( 𝑎 𝐹 𝑠 ) = ( 𝐻 ‘ ( card ‘ 𝑎 ) ) ) )
30 vex ⊢ 𝑥 ∈ V
31 vex ⊢ 𝑟 ∈ V
32 fvex ⊢ ( 𝐻 ‘ ( card ‘ 𝑥 ) ) ∈ V
33 fvex ⊢ ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ∈ V
34 32 33 ifex ⊢ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) ∈ V
35 7 ovmpt4g ⊢ ( ( 𝑥 ∈ V ∧ 𝑟 ∈ V ∧ if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) ∈ V ) → ( 𝑥 𝐹 𝑟 ) = if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) )
36 30 31 34 35 mp3an ⊢ ( 𝑥 𝐹 𝑟 ) = if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) )
37 iftrue ⊢ ( 𝑥 ∈ Fin → if ( 𝑥 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑥 ) ) , ( 𝐷 ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( 𝐷 ‘ 𝑧 ) ∈ 𝑥 } ) ) = ( 𝐻 ‘ ( card ‘ 𝑥 ) ) )
38 36 37 syl5eq ⊢ ( 𝑥 ∈ Fin → ( 𝑥 𝐹 𝑟 ) = ( 𝐻 ‘ ( card ‘ 𝑥 ) ) )
39 38 adantr ⊢ ( ( 𝑥 ∈ Fin ∧ 𝑟 ∈ 𝑉 ) → ( 𝑥 𝐹 𝑟 ) = ( 𝐻 ‘ ( card ‘ 𝑥 ) ) )
40 13 14 15 20 24 27 29 39 vtocl2gaf ⊢ ( ( 𝑎 ∈ Fin ∧ 𝑠 ∈ 𝑉 ) → ( 𝑎 𝐹 𝑠 ) = ( 𝐻 ‘ ( card ‘ 𝑎 ) ) )
41 10 12 40 vtocl2ga ⊢ ( ( 𝑌 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑌 𝐹 𝑅 ) = ( 𝐻 ‘ ( card ‘ 𝑌 ) ) )