This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ackbij1lem8

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 19-Nov-2014)

Ref Expression
Hypothesis ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
Assertion ackbij1lem8 ( 𝐴 ∈ ω → ( 𝐹 ‘ { 𝐴 } ) = ( card ‘ 𝒫 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2 sneq ⊢ ( 𝑎 = 𝐴 → { 𝑎 } = { 𝐴 } )
3 2 fveq2d ⊢ ( 𝑎 = 𝐴 → ( 𝐹 ‘ { 𝑎 } ) = ( 𝐹 ‘ { 𝐴 } ) )
4 pweq ⊢ ( 𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴 )
5 4 fveq2d ⊢ ( 𝑎 = 𝐴 → ( card ‘ 𝒫 𝑎 ) = ( card ‘ 𝒫 𝐴 ) )
6 3 5 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐹 ‘ { 𝑎 } ) = ( card ‘ 𝒫 𝑎 ) ↔ ( 𝐹 ‘ { 𝐴 } ) = ( card ‘ 𝒫 𝐴 ) ) )
7 ackbij1lem4 ⊢ ( 𝑎 ∈ ω → { 𝑎 } ∈ ( 𝒫 ω ∩ Fin ) )
8 1 ackbij1lem7 ⊢ ( { 𝑎 } ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ { 𝑎 } ) = ( card ‘ ∪ 𝑦 ∈ { 𝑎 } ( { 𝑦 } × 𝒫 𝑦 ) ) )
9 7 8 syl ⊢ ( 𝑎 ∈ ω → ( 𝐹 ‘ { 𝑎 } ) = ( card ‘ ∪ 𝑦 ∈ { 𝑎 } ( { 𝑦 } × 𝒫 𝑦 ) ) )
10 vex ⊢ 𝑎 ∈ V
11 sneq ⊢ ( 𝑦 = 𝑎 → { 𝑦 } = { 𝑎 } )
12 pweq ⊢ ( 𝑦 = 𝑎 → 𝒫 𝑦 = 𝒫 𝑎 )
13 11 12 xpeq12d ⊢ ( 𝑦 = 𝑎 → ( { 𝑦 } × 𝒫 𝑦 ) = ( { 𝑎 } × 𝒫 𝑎 ) )
14 10 13 iunxsn ⊢ ∪ 𝑦 ∈ { 𝑎 } ( { 𝑦 } × 𝒫 𝑦 ) = ( { 𝑎 } × 𝒫 𝑎 )
15 14 fveq2i ⊢ ( card ‘ ∪ 𝑦 ∈ { 𝑎 } ( { 𝑦 } × 𝒫 𝑦 ) ) = ( card ‘ ( { 𝑎 } × 𝒫 𝑎 ) )
16 vpwex ⊢ 𝒫 𝑎 ∈ V
17 xpsnen2g ⊢ ( ( 𝑎 ∈ V ∧ 𝒫 𝑎 ∈ V ) → ( { 𝑎 } × 𝒫 𝑎 ) ≈ 𝒫 𝑎 )
18 10 16 17 mp2an ⊢ ( { 𝑎 } × 𝒫 𝑎 ) ≈ 𝒫 𝑎
19 carden2b ⊢ ( ( { 𝑎 } × 𝒫 𝑎 ) ≈ 𝒫 𝑎 → ( card ‘ ( { 𝑎 } × 𝒫 𝑎 ) ) = ( card ‘ 𝒫 𝑎 ) )
20 18 19 ax-mp ⊢ ( card ‘ ( { 𝑎 } × 𝒫 𝑎 ) ) = ( card ‘ 𝒫 𝑎 )
21 15 20 eqtri ⊢ ( card ‘ ∪ 𝑦 ∈ { 𝑎 } ( { 𝑦 } × 𝒫 𝑦 ) ) = ( card ‘ 𝒫 𝑎 )
22 9 21 eqtrdi ⊢ ( 𝑎 ∈ ω → ( 𝐹 ‘ { 𝑎 } ) = ( card ‘ 𝒫 𝑎 ) )
23 6 22 vtoclga ⊢ ( 𝐴 ∈ ω → ( 𝐹 ‘ { 𝐴 } ) = ( card ‘ 𝒫 𝐴 ) )