Theorem dmct

Description: The domain of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016)

	Ref	Expression
Assertion	dmct	⊢ ( 𝐴 ≼ ω → dom 𝐴 ≼ ω )

Proof

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