Theorem cardidm

Description: The cardinality function is idempotent. Proposition 10.11 of TakeutiZaring p. 85. (Contributed by Mario Carneiro, 7-Jan-2013)

	Ref	Expression
Assertion	cardidm	⊢ ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		cardid2	⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
2	1	ensymd	⊢ ( 𝐴 ∈ dom card → 𝐴 ≈ ( card ‘ 𝐴 ) )
3		entr	⊢ ( ( 𝑦 ≈ 𝐴 ∧ 𝐴 ≈ ( card ‘ 𝐴 ) ) → 𝑦 ≈ ( card ‘ 𝐴 ) )
4	3	expcom	⊢ ( 𝐴 ≈ ( card ‘ 𝐴 ) → ( 𝑦 ≈ 𝐴 → 𝑦 ≈ ( card ‘ 𝐴 ) ) )
5	2 4	syl	⊢ ( 𝐴 ∈ dom card → ( 𝑦 ≈ 𝐴 → 𝑦 ≈ ( card ‘ 𝐴 ) ) )
6		entr	⊢ ( ( 𝑦 ≈ ( card ‘ 𝐴 ) ∧ ( card ‘ 𝐴 ) ≈ 𝐴 ) → 𝑦 ≈ 𝐴 )
7	6	expcom	⊢ ( ( card ‘ 𝐴 ) ≈ 𝐴 → ( 𝑦 ≈ ( card ‘ 𝐴 ) → 𝑦 ≈ 𝐴 ) )
8	1 7	syl	⊢ ( 𝐴 ∈ dom card → ( 𝑦 ≈ ( card ‘ 𝐴 ) → 𝑦 ≈ 𝐴 ) )
9	5 8	impbid	⊢ ( 𝐴 ∈ dom card → ( 𝑦 ≈ 𝐴 ↔ 𝑦 ≈ ( card ‘ 𝐴 ) ) )
10	9	rabbidv	⊢ ( 𝐴 ∈ dom card → { 𝑦 ∈ On ∣ 𝑦 ≈ 𝐴 } = { 𝑦 ∈ On ∣ 𝑦 ≈ ( card ‘ 𝐴 ) } )
11	10	inteqd	⊢ ( 𝐴 ∈ dom card → ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ 𝐴 } = ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ ( card ‘ 𝐴 ) } )
12		cardval3	⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ 𝐴 } )
13		cardon	⊢ ( card ‘ 𝐴 ) ∈ On
14		oncardval	⊢ ( ( card ‘ 𝐴 ) ∈ On → ( card ‘ ( card ‘ 𝐴 ) ) = ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ ( card ‘ 𝐴 ) } )
15	13 14	mp1i	⊢ ( 𝐴 ∈ dom card → ( card ‘ ( card ‘ 𝐴 ) ) = ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ ( card ‘ 𝐴 ) } )
16	11 12 15	3eqtr4rd	⊢ ( 𝐴 ∈ dom card → ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) )
17		card0	⊢ ( card ‘ ∅ ) = ∅
18		ndmfv	⊢ ( ¬ 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = ∅ )
19	18	fveq2d	⊢ ( ¬ 𝐴 ∈ dom card → ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ ∅ ) )
20	17 19 18	3eqtr4a	⊢ ( ¬ 𝐴 ∈ dom card → ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) )
21	16 20	pm2.61i	⊢ ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 )