fnfi

Description: A version of fnex for finite sets that does not require Replacement or Power Sets. (Contributed by Mario Carneiro, 16-Nov-2014) (Revised by Mario Carneiro, 24-Jun-2015)

		Ref	Expression
	Assertion	fnfi	$⊢ (F Fn A \land A \in Fin) \to F \in Fin$

Proof

Step	Hyp	Ref	Expression
1		fnresdm	$⊢ F Fn A \to {F ↾}_{A} = F$
2	1	adantr	$⊢ (F Fn A \land A \in Fin) \to {F ↾}_{A} = F$
3		reseq2	$⊢ x = \emptyset \to {F ↾}_{x} = {F ↾}_{\emptyset}$
4	3	eleq1d	$⊢ x = \emptyset \to ({F ↾}_{x} \in Fin \leftrightarrow {F ↾}_{\emptyset} \in Fin)$
5	4	imbi2d	$⊢ x = \emptyset \to (((F Fn A \land A \in Fin) \to {F ↾}_{x} \in Fin) \leftrightarrow ((F Fn A \land A \in Fin) \to {F ↾}_{\emptyset} \in Fin))$
6		reseq2	$⊢ x = y \to {F ↾}_{x} = {F ↾}_{y}$
7	6	eleq1d	$⊢ x = y \to ({F ↾}_{x} \in Fin \leftrightarrow {F ↾}_{y} \in Fin)$
8	7	imbi2d	$⊢ x = y \to (((F Fn A \land A \in Fin) \to {F ↾}_{x} \in Fin) \leftrightarrow ((F Fn A \land A \in Fin) \to {F ↾}_{y} \in Fin))$
9		reseq2	$⊢ x = y \cup \{z\} \to {F ↾}_{x} = {F ↾}_{(y \cup \{z\})}$
10	9	eleq1d	$⊢ x = y \cup \{z\} \to ({F ↾}_{x} \in Fin \leftrightarrow {F ↾}_{(y \cup \{z\})} \in Fin)$
11	10	imbi2d	$⊢ x = y \cup \{z\} \to (((F Fn A \land A \in Fin) \to {F ↾}_{x} \in Fin) \leftrightarrow ((F Fn A \land A \in Fin) \to {F ↾}_{(y \cup \{z\})} \in Fin))$
12		reseq2	$⊢ x = A \to {F ↾}_{x} = {F ↾}_{A}$
13	12	eleq1d	$⊢ x = A \to ({F ↾}_{x} \in Fin \leftrightarrow {F ↾}_{A} \in Fin)$
14	13	imbi2d	$⊢ x = A \to (((F Fn A \land A \in Fin) \to {F ↾}_{x} \in Fin) \leftrightarrow ((F Fn A \land A \in Fin) \to {F ↾}_{A} \in Fin))$
15		res0	$⊢ {F ↾}_{\emptyset} = \emptyset$
16		0fin	$⊢ \emptyset \in Fin$
17	15 16	eqeltri	$⊢ {F ↾}_{\emptyset} \in Fin$
18	17	a1i	$⊢ (F Fn A \land A \in Fin) \to {F ↾}_{\emptyset} \in Fin$
19		resundi	$⊢ {F ↾}_{(y \cup \{z\})} = ({F ↾}_{y}) \cup ({F ↾}_{\{z\}})$
20		snfi	$⊢ \{⟨z, F (z)⟩\} \in Fin$
21		fnfun	$⊢ F Fn A \to Fun F$
22		funressn	$⊢ Fun F \to {F ↾}_{\{z\}} \subseteq \{⟨z, F (z)⟩\}$
23	21 22	syl	$⊢ F Fn A \to {F ↾}_{\{z\}} \subseteq \{⟨z, F (z)⟩\}$
24	23	adantr	$⊢ (F Fn A \land A \in Fin) \to {F ↾}_{\{z\}} \subseteq \{⟨z, F (z)⟩\}$
25		ssfi	$⊢ (\{⟨z, F (z)⟩\} \in Fin \land {F ↾}_{\{z\}} \subseteq \{⟨z, F (z)⟩\}) \to {F ↾}_{\{z\}} \in Fin$
26	20 24 25	sylancr	$⊢ (F Fn A \land A \in Fin) \to {F ↾}_{\{z\}} \in Fin$
27		unfi	$⊢ ({F ↾}_{y} \in Fin \land {F ↾}_{\{z\}} \in Fin) \to ({F ↾}_{y}) \cup ({F ↾}_{\{z\}}) \in Fin$
28	26 27	sylan2	$⊢ ({F ↾}_{y} \in Fin \land (F Fn A \land A \in Fin)) \to ({F ↾}_{y}) \cup ({F ↾}_{\{z\}}) \in Fin$
29	19 28	eqeltrid	$⊢ ({F ↾}_{y} \in Fin \land (F Fn A \land A \in Fin)) \to {F ↾}_{(y \cup \{z\})} \in Fin$
30	29	expcom	$⊢ (F Fn A \land A \in Fin) \to ({F ↾}_{y} \in Fin \to {F ↾}_{(y \cup \{z\})} \in Fin)$
31	30	a2i	$⊢ ((F Fn A \land A \in Fin) \to {F ↾}_{y} \in Fin) \to ((F Fn A \land A \in Fin) \to {F ↾}_{(y \cup \{z\})} \in Fin)$
32	31	a1i	$⊢ y \in Fin \to (((F Fn A \land A \in Fin) \to {F ↾}_{y} \in Fin) \to ((F Fn A \land A \in Fin) \to {F ↾}_{(y \cup \{z\})} \in Fin))$
33	5 8 11 14 18 32	findcard2	$⊢ A \in Fin \to ((F Fn A \land A \in Fin) \to {F ↾}_{A} \in Fin)$
34	33	anabsi7	$⊢ (F Fn A \land A \in Fin) \to {F ↾}_{A} \in Fin$
35	2 34	eqeltrrd	$⊢ (F Fn A \land A \in Fin) \to F \in Fin$

Metamath Proof Explorer

Theorem fnfi

Proof