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 ‘ 𝒫 𝐴 ) )