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	$⊢ A \in dom card \to (Fun F \to F [A] ≼ A)$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
2		inss1	$⊢ A \cap dom F \subseteq A$
3		ssnum	$⊢ (A \in dom card \land A \cap dom F \subseteq A) \to A \cap dom F \in dom card$
4	2 3	mpan2	$⊢ A \in dom card \to A \cap dom F \in dom card$
5	4	adantr	$⊢ (A \in dom card \land Fun F) \to A \cap dom F \in dom card$
6		funres	$⊢ Fun F \to Fun ({F ↾}_{A})$
7		funfn	$⊢ Fun ({F ↾}_{A}) \leftrightarrow ({F ↾}_{A}) Fn dom ({F ↾}_{A})$
8	6 7	sylib	$⊢ Fun F \to ({F ↾}_{A}) Fn dom ({F ↾}_{A})$
9		dmres	$⊢ dom ({F ↾}_{A}) = A \cap dom F$
10	9	fneq2i	$⊢ ({F ↾}_{A}) Fn dom ({F ↾}_{A}) \leftrightarrow ({F ↾}_{A}) Fn (A \cap dom F)$
11	8 10	sylib	$⊢ Fun F \to ({F ↾}_{A}) Fn (A \cap dom F)$
12	11	adantl	$⊢ (A \in dom card \land Fun F) \to ({F ↾}_{A}) Fn (A \cap dom F)$
13		dffn4	$⊢ ({F ↾}_{A}) Fn (A \cap dom F) \leftrightarrow ({F ↾}_{A}) : A \cap dom F \underset{onto}{⟶} ran ({F ↾}_{A})$
14		fodomnum	$⊢ A \cap dom F \in dom card \to (({F ↾}_{A}) : A \cap dom F \underset{onto}{⟶} ran ({F ↾}_{A}) \to ran ({F ↾}_{A}) ≼ (A \cap dom F))$
15	13 14	biimtrid	$⊢ A \cap dom F \in dom card \to (({F ↾}_{A}) Fn (A \cap dom F) \to ran ({F ↾}_{A}) ≼ (A \cap dom F))$
16	5 12 15	sylc	$⊢ (A \in dom card \land Fun F) \to ran ({F ↾}_{A}) ≼ (A \cap dom F)$
17	1 16	eqbrtrid	$⊢ (A \in dom card \land Fun F) \to F [A] ≼ (A \cap dom F)$
18		elex	$⊢ A \in dom card \to A \in V$
19		ssdomg	$⊢ A \in V \to (A \cap dom F \subseteq A \to (A \cap dom F) ≼ A)$
20	18 19	syl	$⊢ A \in dom card \to (A \cap dom F \subseteq A \to (A \cap dom F) ≼ A)$
21	2 20	mpi	$⊢ A \in dom card \to (A \cap dom F) ≼ A$
22	21	adantr	$⊢ (A \in dom card \land Fun F) \to (A \cap dom F) ≼ A$
23		domtr	$⊢ (F [A] ≼ (A \cap dom F) \land (A \cap dom F) ≼ A) \to F [A] ≼ A$
24	17 22 23	syl2anc	$⊢ (A \in dom card \land Fun F) \to F [A] ≼ A$
25	24	ex	$⊢ A \in dom card \to (Fun F \to F [A] ≼ A)$

Metamath Proof Explorer

Theorem imadomnum

Proof