Theorem iscard4

Description: Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023)

	Ref	Expression
Assertion	iscard4	⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ 𝐴 ∈ ran card )

Proof

Step	Hyp	Ref	Expression
1		eqcom	⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ 𝐴 = ( card ‘ 𝐴 ) )
2		mptrel	⊢ Rel ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ 𝑥 } )
3		df-card	⊢ card = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ 𝑥 } )
4	3	releqi	⊢ ( Rel card ↔ Rel ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ 𝑥 } ) )
5	2 4	mpbir	⊢ Rel card
6		relelrnb	⊢ ( Rel card → ( 𝐴 ∈ ran card ↔ ∃ 𝑥 𝑥 card 𝐴 ) )
7	5 6	ax-mp	⊢ ( 𝐴 ∈ ran card ↔ ∃ 𝑥 𝑥 card 𝐴 )
8	3	funmpt2	⊢ Fun card
9		funbrfv	⊢ ( Fun card → ( 𝑥 card 𝐴 → ( card ‘ 𝑥 ) = 𝐴 ) )
10	8 9	ax-mp	⊢ ( 𝑥 card 𝐴 → ( card ‘ 𝑥 ) = 𝐴 )
11	10	eqcomd	⊢ ( 𝑥 card 𝐴 → 𝐴 = ( card ‘ 𝑥 ) )
12	11	eximi	⊢ ( ∃ 𝑥 𝑥 card 𝐴 → ∃ 𝑥 𝐴 = ( card ‘ 𝑥 ) )
13		cardidm	⊢ ( card ‘ ( card ‘ 𝑥 ) ) = ( card ‘ 𝑥 )
14		fveq2	⊢ ( 𝐴 = ( card ‘ 𝑥 ) → ( card ‘ 𝐴 ) = ( card ‘ ( card ‘ 𝑥 ) ) )
15		id	⊢ ( 𝐴 = ( card ‘ 𝑥 ) → 𝐴 = ( card ‘ 𝑥 ) )
16	13 14 15	3eqtr4a	⊢ ( 𝐴 = ( card ‘ 𝑥 ) → ( card ‘ 𝐴 ) = 𝐴 )
17	16	exlimiv	⊢ ( ∃ 𝑥 𝐴 = ( card ‘ 𝑥 ) → ( card ‘ 𝐴 ) = 𝐴 )
18	1	biimpi	⊢ ( ( card ‘ 𝐴 ) = 𝐴 → 𝐴 = ( card ‘ 𝐴 ) )
19		cardon	⊢ ( card ‘ 𝐴 ) ∈ On
20	18 19	eqeltrdi	⊢ ( ( card ‘ 𝐴 ) = 𝐴 → 𝐴 ∈ On )
21		onenon	⊢ ( 𝐴 ∈ On → 𝐴 ∈ dom card )
22	20 21	syl	⊢ ( ( card ‘ 𝐴 ) = 𝐴 → 𝐴 ∈ dom card )
23		funfvbrb	⊢ ( Fun card → ( 𝐴 ∈ dom card ↔ 𝐴 card ( card ‘ 𝐴 ) ) )
24	23	biimpd	⊢ ( Fun card → ( 𝐴 ∈ dom card → 𝐴 card ( card ‘ 𝐴 ) ) )
25	8 22 24	mpsyl	⊢ ( ( card ‘ 𝐴 ) = 𝐴 → 𝐴 card ( card ‘ 𝐴 ) )
26		id	⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( card ‘ 𝐴 ) = 𝐴 )
27	25 26	breqtrd	⊢ ( ( card ‘ 𝐴 ) = 𝐴 → 𝐴 card 𝐴 )
28		id	⊢ ( 𝐴 = ( card ‘ 𝐴 ) → 𝐴 = ( card ‘ 𝐴 ) )
29	28 19	eqeltrdi	⊢ ( 𝐴 = ( card ‘ 𝐴 ) → 𝐴 ∈ On )
30	29	eqcoms	⊢ ( ( card ‘ 𝐴 ) = 𝐴 → 𝐴 ∈ On )
31		sbcbr1g	⊢ ( 𝐴 ∈ On → ( [ 𝐴 / 𝑥 ] 𝑥 card 𝐴 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑥 card 𝐴 ) )
32		csbvarg	⊢ ( 𝐴 ∈ On → ⦋ 𝐴 / 𝑥 ⦌ 𝑥 = 𝐴 )
33	32	breq1d	⊢ ( 𝐴 ∈ On → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑥 card 𝐴 ↔ 𝐴 card 𝐴 ) )
34	31 33	bitrd	⊢ ( 𝐴 ∈ On → ( [ 𝐴 / 𝑥 ] 𝑥 card 𝐴 ↔ 𝐴 card 𝐴 ) )
35	30 34	syl	⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( [ 𝐴 / 𝑥 ] 𝑥 card 𝐴 ↔ 𝐴 card 𝐴 ) )
36	27 35	mpbird	⊢ ( ( card ‘ 𝐴 ) = 𝐴 → [ 𝐴 / 𝑥 ] 𝑥 card 𝐴 )
37	36	spesbcd	⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ∃ 𝑥 𝑥 card 𝐴 )
38	17 37	syl	⊢ ( ∃ 𝑥 𝐴 = ( card ‘ 𝑥 ) → ∃ 𝑥 𝑥 card 𝐴 )
39	12 38	impbii	⊢ ( ∃ 𝑥 𝑥 card 𝐴 ↔ ∃ 𝑥 𝐴 = ( card ‘ 𝑥 ) )
40		oncard	⊢ ( ∃ 𝑥 𝐴 = ( card ‘ 𝑥 ) ↔ 𝐴 = ( card ‘ 𝐴 ) )
41	7 39 40	3bitrri	⊢ ( 𝐴 = ( card ‘ 𝐴 ) ↔ 𝐴 ∈ ran card )
42	1 41	bitri	⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ 𝐴 ∈ ran card )