Theorem imadomnum

Description: A version of imadomg that does not require the axiom of choice ax-ac . (Contributed by Vincent Gonzalez, 25-Aug-2026)

	Ref	Expression
Assertion	imadomnum	⊢ ( 𝐴 ∈ dom card → ( Fun 𝐹 → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
2		inss1	⊢ ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴
3		ssnum	⊢ ( ( 𝐴 ∈ dom card ∧ ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴 ) → ( 𝐴 ∩ dom 𝐹 ) ∈ dom card )
4	2 3	mpan2	⊢ ( 𝐴 ∈ dom card → ( 𝐴 ∩ dom 𝐹 ) ∈ dom card )
5	4	adantr	⊢ ( ( 𝐴 ∈ dom card ∧ Fun 𝐹 ) → ( 𝐴 ∩ dom 𝐹 ) ∈ dom card )
6		funres	⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝐴 ) )
7		funfn	⊢ ( Fun ( 𝐹 ↾ 𝐴 ) ↔ ( 𝐹 ↾ 𝐴 ) Fn dom ( 𝐹 ↾ 𝐴 ) )
8	6 7	sylib	⊢ ( Fun 𝐹 → ( 𝐹 ↾ 𝐴 ) Fn dom ( 𝐹 ↾ 𝐴 ) )
9		dmres	⊢ dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 )
10	9	fneq2i	⊢ ( ( 𝐹 ↾ 𝐴 ) Fn dom ( 𝐹 ↾ 𝐴 ) ↔ ( 𝐹 ↾ 𝐴 ) Fn ( 𝐴 ∩ dom 𝐹 ) )
11	8 10	sylib	⊢ ( Fun 𝐹 → ( 𝐹 ↾ 𝐴 ) Fn ( 𝐴 ∩ dom 𝐹 ) )
12	11	adantl	⊢ ( ( 𝐴 ∈ dom card ∧ Fun 𝐹 ) → ( 𝐹 ↾ 𝐴 ) Fn ( 𝐴 ∩ dom 𝐹 ) )
13		dffn4	⊢ ( ( 𝐹 ↾ 𝐴 ) Fn ( 𝐴 ∩ dom 𝐹 ) ↔ ( 𝐹 ↾ 𝐴 ) : ( 𝐴 ∩ dom 𝐹 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) )
14		fodomnum	⊢ ( ( 𝐴 ∩ dom 𝐹 ) ∈ dom card → ( ( 𝐹 ↾ 𝐴 ) : ( 𝐴 ∩ dom 𝐹 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) → ran ( 𝐹 ↾ 𝐴 ) ≼ ( 𝐴 ∩ dom 𝐹 ) ) )
15	13 14	biimtrid	⊢ ( ( 𝐴 ∩ dom 𝐹 ) ∈ dom card → ( ( 𝐹 ↾ 𝐴 ) Fn ( 𝐴 ∩ dom 𝐹 ) → ran ( 𝐹 ↾ 𝐴 ) ≼ ( 𝐴 ∩ dom 𝐹 ) ) )
16	5 12 15	sylc	⊢ ( ( 𝐴 ∈ dom card ∧ Fun 𝐹 ) → ran ( 𝐹 ↾ 𝐴 ) ≼ ( 𝐴 ∩ dom 𝐹 ) )
17	1 16	eqbrtrid	⊢ ( ( 𝐴 ∈ dom card ∧ Fun 𝐹 ) → ( 𝐹 “ 𝐴 ) ≼ ( 𝐴 ∩ dom 𝐹 ) )
18		elex	⊢ ( 𝐴 ∈ dom card → 𝐴 ∈ V )
19		ssdomg	⊢ ( 𝐴 ∈ V → ( ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴 → ( 𝐴 ∩ dom 𝐹 ) ≼ 𝐴 ) )
20	18 19	syl	⊢ ( 𝐴 ∈ dom card → ( ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴 → ( 𝐴 ∩ dom 𝐹 ) ≼ 𝐴 ) )
21	2 20	mpi	⊢ ( 𝐴 ∈ dom card → ( 𝐴 ∩ dom 𝐹 ) ≼ 𝐴 )
22	21	adantr	⊢ ( ( 𝐴 ∈ dom card ∧ Fun 𝐹 ) → ( 𝐴 ∩ dom 𝐹 ) ≼ 𝐴 )
23		domtr	⊢ ( ( ( 𝐹 “ 𝐴 ) ≼ ( 𝐴 ∩ dom 𝐹 ) ∧ ( 𝐴 ∩ dom 𝐹 ) ≼ 𝐴 ) → ( 𝐹 “ 𝐴 ) ≼ 𝐴 )
24	17 22 23	syl2anc	⊢ ( ( 𝐴 ∈ dom card ∧ Fun 𝐹 ) → ( 𝐹 “ 𝐴 ) ≼ 𝐴 )
25	24	ex	⊢ ( 𝐴 ∈ dom card → ( Fun 𝐹 → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) )