imafi

Description: Images of finite sets are finite. For a shorter proof using ax-pow , see imafiALT . (Contributed by Stefan O'Rear, 22-Feb-2015) Avoid ax-pow . (Revised by BTernaryTau, 7-Sep-2024)

		Ref	Expression
	Assertion	imafi	$⊢ (Fun F \land X \in Fin) \to F [X] \in Fin$

Proof

Step	Hyp	Ref	Expression
1		imaeq2	$⊢ x = \emptyset \to F [x] = F [\emptyset]$
2	1	eleq1d	$⊢ x = \emptyset \to (F [x] \in Fin \leftrightarrow F [\emptyset] \in Fin)$
3	2	imbi2d	$⊢ x = \emptyset \to ((Fun F \to F [x] \in Fin) \leftrightarrow (Fun F \to F [\emptyset] \in Fin))$
4		imaeq2	$⊢ x = y \to F [x] = F [y]$
5	4	eleq1d	$⊢ x = y \to (F [x] \in Fin \leftrightarrow F [y] \in Fin)$
6	5	imbi2d	$⊢ x = y \to ((Fun F \to F [x] \in Fin) \leftrightarrow (Fun F \to F [y] \in Fin))$
7		imaeq2	$⊢ x = y \cup \{z\} \to F [x] = F [y \cup \{z\}]$
8	7	eleq1d	$⊢ x = y \cup \{z\} \to (F [x] \in Fin \leftrightarrow F [y \cup \{z\}] \in Fin)$
9	8	imbi2d	$⊢ x = y \cup \{z\} \to ((Fun F \to F [x] \in Fin) \leftrightarrow (Fun F \to F [y \cup \{z\}] \in Fin))$
10		imaeq2	$⊢ x = X \to F [x] = F [X]$
11	10	eleq1d	$⊢ x = X \to (F [x] \in Fin \leftrightarrow F [X] \in Fin)$
12	11	imbi2d	$⊢ x = X \to ((Fun F \to F [x] \in Fin) \leftrightarrow (Fun F \to F [X] \in Fin))$
13		ima0	$⊢ F [\emptyset] = \emptyset$
14		0fin	$⊢ \emptyset \in Fin$
15	13 14	eqeltri	$⊢ F [\emptyset] \in Fin$
16	15	a1i	$⊢ Fun F \to F [\emptyset] \in Fin$
17		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
18		fnsnfv	$⊢ (F Fn dom F \land z \in dom F) \to \{F (z)\} = F [\{z\}]$
19	17 18	sylanb	$⊢ (Fun F \land z \in dom F) \to \{F (z)\} = F [\{z\}]$
20		snfi	$⊢ \{F (z)\} \in Fin$
21	19 20	eqeltrrdi	$⊢ (Fun F \land z \in dom F) \to F [\{z\}] \in Fin$
22		ndmima	$⊢ \neg z \in dom F \to F [\{z\}] = \emptyset$
23	22 14	eqeltrdi	$⊢ \neg z \in dom F \to F [\{z\}] \in Fin$
24	23	adantl	$⊢ (Fun F \land \neg z \in dom F) \to F [\{z\}] \in Fin$
25	21 24	pm2.61dan	$⊢ Fun F \to F [\{z\}] \in Fin$
26		imaundi	$⊢ F [y \cup \{z\}] = F [y] \cup F [\{z\}]$
27		unfi	$⊢ (F [y] \in Fin \land F [\{z\}] \in Fin) \to F [y] \cup F [\{z\}] \in Fin$
28	26 27	eqeltrid	$⊢ (F [y] \in Fin \land F [\{z\}] \in Fin) \to F [y \cup \{z\}] \in Fin$
29	25 28	sylan2	$⊢ (F [y] \in Fin \land Fun F) \to F [y \cup \{z\}] \in Fin$
30	29	expcom	$⊢ Fun F \to (F [y] \in Fin \to F [y \cup \{z\}] \in Fin)$
31	30	a2i	$⊢ (Fun F \to F [y] \in Fin) \to (Fun F \to F [y \cup \{z\}] \in Fin)$
32	31	a1i	$⊢ y \in Fin \to ((Fun F \to F [y] \in Fin) \to (Fun F \to F [y \cup \{z\}] \in Fin))$
33	3 6 9 12 16 32	findcard2	$⊢ X \in Fin \to (Fun F \to F [X] \in Fin)$
34	33	impcom	$⊢ (Fun F \land X \in Fin) \to F [X] \in Fin$

Metamath Proof Explorer

Theorem imafi

Proof