Theorem dmct

Description: The domain of a countable set is countable. The proof uses fodomnum rather than fodomg , and so does not require ax-ac . (Contributed by Thierry Arnoux, 29-Dec-2016) (Revised by Vincent Gonzalez, 24-Aug-2026)

	Ref	Expression
Assertion	dmct	|- ( A ~<_ _om -> dom A ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		dmresv	|- dom ( A |` _V ) = dom A
2		omelon	|- _om e. On
3	2	a1i	|- ( A ~<_ _om -> _om e. On )
4		id	|- ( A ~<_ _om -> A ~<_ _om )
5		ondomen	|- ( ( _om e. On /\ A ~<_ _om ) -> A e. dom card )
6	3 4 5	syl2anc	|- ( A ~<_ _om -> A e. dom card )
7		resss	|- ( A |` _V ) C_ A
8	7	a1i	|- ( A ~<_ _om -> ( A |` _V ) C_ A )
9		ssnum	|- ( ( A e. dom card /\ ( A |` _V ) C_ A ) -> ( A |` _V ) e. dom card )
10	6 8 9	syl2anc	|- ( A ~<_ _om -> ( A |` _V ) e. dom card )
11		fvex	|- ( 1st ` x ) e. _V
12		eqid	|- ( x e. ( A |` _V ) |-> ( 1st ` x ) ) = ( x e. ( A |` _V ) |-> ( 1st ` x ) )
13	11 12	fnmpti	|- ( x e. ( A |` _V ) |-> ( 1st ` x ) ) Fn ( A |` _V )
14		dffn4	|- ( ( x e. ( A |` _V ) |-> ( 1st ` x ) ) Fn ( A |` _V ) <-> ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> ran ( x e. ( A |` _V ) |-> ( 1st ` x ) ) )
15	13 14	mpbi	|- ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> ran ( x e. ( A |` _V ) |-> ( 1st ` x ) )
16		relres	|- Rel ( A |` _V )
17		reldm	|- ( Rel ( A |` _V ) -> dom ( A |` _V ) = ran ( x e. ( A |` _V ) |-> ( 1st ` x ) ) )
18		foeq3	|- ( dom ( A |` _V ) = ran ( x e. ( A |` _V ) |-> ( 1st ` x ) ) -> ( ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> dom ( A |` _V ) <-> ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> ran ( x e. ( A |` _V ) |-> ( 1st ` x ) ) ) )
19	16 17 18	mp2b	|- ( ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> dom ( A |` _V ) <-> ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> ran ( x e. ( A |` _V ) |-> ( 1st ` x ) ) )
20	15 19	mpbir	|- ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> dom ( A |` _V )
21		fodomnum	|- ( ( A |` _V ) e. dom card -> ( ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> dom ( A |` _V ) -> dom ( A |` _V ) ~<_ ( A |` _V ) ) )
22	10 20 21	mpisyl	|- ( A ~<_ _om -> dom ( A |` _V ) ~<_ ( A |` _V ) )
23		ctex	|- ( A ~<_ _om -> A e. _V )
24		ssdomg	|- ( A e. _V -> ( ( A |` _V ) C_ A -> ( A |` _V ) ~<_ A ) )
25	23 7 24	mpisyl	|- ( A ~<_ _om -> ( A |` _V ) ~<_ A )
26		domtr	|- ( ( ( A |` _V ) ~<_ A /\ A ~<_ _om ) -> ( A |` _V ) ~<_ _om )
27	25 26	mpancom	|- ( A ~<_ _om -> ( A |` _V ) ~<_ _om )
28		domtr	|- ( ( dom ( A |` _V ) ~<_ ( A |` _V ) /\ ( A |` _V ) ~<_ _om ) -> dom ( A |` _V ) ~<_ _om )
29	22 27 28	syl2anc	|- ( A ~<_ _om -> dom ( A |` _V ) ~<_ _om )
30	1 29	eqbrtrrid	|- ( A ~<_ _om -> dom A ~<_ _om )