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	⊢ ( 𝐴 ≼ ω → dom 𝐴 ≼ ω )

Proof

Step	Hyp	Ref	Expression
1		dmresv	⊢ dom ( 𝐴 ↾ V ) = dom 𝐴
2		omelon	⊢ ω ∈ On
3	2	a1i	⊢ ( 𝐴 ≼ ω → ω ∈ On )
4		id	⊢ ( 𝐴 ≼ ω → 𝐴 ≼ ω )
5		ondomen	⊢ ( ( ω ∈ On ∧ 𝐴 ≼ ω ) → 𝐴 ∈ dom card )
6	3 4 5	syl2anc	⊢ ( 𝐴 ≼ ω → 𝐴 ∈ dom card )
7		resss	⊢ ( 𝐴 ↾ V ) ⊆ 𝐴
8	7	a1i	⊢ ( 𝐴 ≼ ω → ( 𝐴 ↾ V ) ⊆ 𝐴 )
9		ssnum	⊢ ( ( 𝐴 ∈ dom card ∧ ( 𝐴 ↾ V ) ⊆ 𝐴 ) → ( 𝐴 ↾ V ) ∈ dom card )
10	6 8 9	syl2anc	⊢ ( 𝐴 ≼ ω → ( 𝐴 ↾ V ) ∈ dom card )
11		fvex	⊢ ( 1^st ‘ 𝑥 ) ∈ V
12		eqid	⊢ ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) )
13	11 12	fnmpti	⊢ ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) Fn ( 𝐴 ↾ V )
14		dffn4	⊢ ( ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) Fn ( 𝐴 ↾ V ) ↔ ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) : ( 𝐴 ↾ V ) –onto→ ran ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) )
15	13 14	mpbi	⊢ ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) : ( 𝐴 ↾ V ) –onto→ ran ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) )
16		relres	⊢ Rel ( 𝐴 ↾ V )
17		reldm	⊢ ( Rel ( 𝐴 ↾ V ) → dom ( 𝐴 ↾ V ) = ran ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) )
18		foeq3	⊢ ( dom ( 𝐴 ↾ V ) = ran ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) → ( ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) : ( 𝐴 ↾ V ) –onto→ dom ( 𝐴 ↾ V ) ↔ ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) : ( 𝐴 ↾ V ) –onto→ ran ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) ) )
19	16 17 18	mp2b	⊢ ( ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) : ( 𝐴 ↾ V ) –onto→ dom ( 𝐴 ↾ V ) ↔ ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) : ( 𝐴 ↾ V ) –onto→ ran ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) )
20	15 19	mpbir	⊢ ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) : ( 𝐴 ↾ V ) –onto→ dom ( 𝐴 ↾ V )
21		fodomnum	⊢ ( ( 𝐴 ↾ V ) ∈ dom card → ( ( 𝑥 ∈ ( 𝐴 ↾ V ) ↦ ( 1^st ‘ 𝑥 ) ) : ( 𝐴 ↾ V ) –onto→ dom ( 𝐴 ↾ V ) → dom ( 𝐴 ↾ V ) ≼ ( 𝐴 ↾ V ) ) )
22	10 20 21	mpisyl	⊢ ( 𝐴 ≼ ω → dom ( 𝐴 ↾ V ) ≼ ( 𝐴 ↾ V ) )
23		ctex	⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V )
24		ssdomg	⊢ ( 𝐴 ∈ V → ( ( 𝐴 ↾ V ) ⊆ 𝐴 → ( 𝐴 ↾ V ) ≼ 𝐴 ) )
25	23 7 24	mpisyl	⊢ ( 𝐴 ≼ ω → ( 𝐴 ↾ V ) ≼ 𝐴 )
26		domtr	⊢ ( ( ( 𝐴 ↾ V ) ≼ 𝐴 ∧ 𝐴 ≼ ω ) → ( 𝐴 ↾ V ) ≼ ω )
27	25 26	mpancom	⊢ ( 𝐴 ≼ ω → ( 𝐴 ↾ V ) ≼ ω )
28		domtr	⊢ ( ( dom ( 𝐴 ↾ V ) ≼ ( 𝐴 ↾ V ) ∧ ( 𝐴 ↾ V ) ≼ ω ) → dom ( 𝐴 ↾ V ) ≼ ω )
29	22 27 28	syl2anc	⊢ ( 𝐴 ≼ ω → dom ( 𝐴 ↾ V ) ≼ ω )
30	1 29	eqbrtrrid	⊢ ( 𝐴 ≼ ω → dom 𝐴 ≼ ω )

Metamath Proof Explorer

Theorem dmct

Proof