fnchoice

Description: For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017)

		Ref	Expression
	Assertion	fnchoice	$⊢ A \in Fin \to \exists f (f Fn A \land \forall x \in A (x \neq \emptyset \to f (x) \in x))$

Proof

Step	Hyp	Ref	Expression
1		fneq2	$⊢ w = \emptyset \to (f Fn w \leftrightarrow f Fn \emptyset)$
2		raleq	$⊢ w = \emptyset \to (\forall x \in w (x \neq \emptyset \to f (x) \in x) \leftrightarrow \forall x \in \emptyset (x \neq \emptyset \to f (x) \in x))$
3	1 2	anbi12d	$⊢ w = \emptyset \to ((f Fn w \land \forall x \in w (x \neq \emptyset \to f (x) \in x)) \leftrightarrow (f Fn \emptyset \land \forall x \in \emptyset (x \neq \emptyset \to f (x) \in x)))$
4	3	exbidv	$⊢ w = \emptyset \to (\exists f (f Fn w \land \forall x \in w (x \neq \emptyset \to f (x) \in x)) \leftrightarrow \exists f (f Fn \emptyset \land \forall x \in \emptyset (x \neq \emptyset \to f (x) \in x)))$
5		fneq2	$⊢ w = y \to (f Fn w \leftrightarrow f Fn y)$
6		raleq	$⊢ w = y \to (\forall x \in w (x \neq \emptyset \to f (x) \in x) \leftrightarrow \forall x \in y (x \neq \emptyset \to f (x) \in x))$
7	5 6	anbi12d	$⊢ w = y \to ((f Fn w \land \forall x \in w (x \neq \emptyset \to f (x) \in x)) \leftrightarrow (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))$
8	7	exbidv	$⊢ w = y \to (\exists f (f Fn w \land \forall x \in w (x \neq \emptyset \to f (x) \in x)) \leftrightarrow \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))$
9		fneq2	$⊢ w = y \cup \{z\} \to (f Fn w \leftrightarrow f Fn (y \cup \{z\}))$
10		raleq	$⊢ w = y \cup \{z\} \to (\forall x \in w (x \neq \emptyset \to f (x) \in x) \leftrightarrow \forall x \in (y \cup \{z\}) (x \neq \emptyset \to f (x) \in x))$
11	9 10	anbi12d	$⊢ w = y \cup \{z\} \to ((f Fn w \land \forall x \in w (x \neq \emptyset \to f (x) \in x)) \leftrightarrow (f Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to f (x) \in x)))$
12	11	exbidv	$⊢ w = y \cup \{z\} \to (\exists f (f Fn w \land \forall x \in w (x \neq \emptyset \to f (x) \in x)) \leftrightarrow \exists f (f Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to f (x) \in x)))$
13		fneq2	$⊢ w = A \to (f Fn w \leftrightarrow f Fn A)$
14		raleq	$⊢ w = A \to (\forall x \in w (x \neq \emptyset \to f (x) \in x) \leftrightarrow \forall x \in A (x \neq \emptyset \to f (x) \in x))$
15	13 14	anbi12d	$⊢ w = A \to ((f Fn w \land \forall x \in w (x \neq \emptyset \to f (x) \in x)) \leftrightarrow (f Fn A \land \forall x \in A (x \neq \emptyset \to f (x) \in x)))$
16	15	exbidv	$⊢ w = A \to (\exists f (f Fn w \land \forall x \in w (x \neq \emptyset \to f (x) \in x)) \leftrightarrow \exists f (f Fn A \land \forall x \in A (x \neq \emptyset \to f (x) \in x)))$
17		0ex	$⊢ \emptyset \in V$
18		fneq1	$⊢ f = \emptyset \to (f Fn \emptyset \leftrightarrow \emptyset Fn \emptyset)$
19		eqid	$⊢ \emptyset = \emptyset$
20		fn0	$⊢ \emptyset Fn \emptyset \leftrightarrow \emptyset = \emptyset$
21	19 20	mpbir	$⊢ \emptyset Fn \emptyset$
22	17 18 21	ceqsexv2d	$⊢ \exists f f Fn \emptyset$
23		ral0	$⊢ \forall x \in \emptyset (x \neq \emptyset \to f (x) \in x)$
24	22 23	exan	$⊢ \exists f (f Fn \emptyset \land \forall x \in \emptyset (x \neq \emptyset \to f (x) \in x))$
25		dffn2	$⊢ f Fn y \leftrightarrow f : y ⟶ V$
26	25	biimpi	$⊢ f Fn y \to f : y ⟶ V$
27	26	ad2antrl	$⊢ (((y \in Fin \land \neg z \in y) \land z = \emptyset) \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to f : y ⟶ V$
28		vex	$⊢ z \in V$
29	28	a1i	$⊢ (((y \in Fin \land \neg z \in y) \land z = \emptyset) \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to z \in V$
30		simpllr	$⊢ (((y \in Fin \land \neg z \in y) \land z = \emptyset) \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to \neg z \in y$
31		vex	$⊢ w \in V$
32	31	a1i	$⊢ (((y \in Fin \land \neg z \in y) \land z = \emptyset) \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to w \in V$
33		fsnunf	$⊢ (f : y ⟶ V \land (z \in V \land \neg z \in y) \land w \in V) \to (f \cup \{⟨z, w⟩\}) : y \cup \{z\} ⟶ V$
34	27 29 30 32 33	syl121anc	$⊢ (((y \in Fin \land \neg z \in y) \land z = \emptyset) \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to (f \cup \{⟨z, w⟩\}) : y \cup \{z\} ⟶ V$
35		dffn2	$⊢ (f \cup \{⟨z, w⟩\}) Fn (y \cup \{z\}) \leftrightarrow (f \cup \{⟨z, w⟩\}) : y \cup \{z\} ⟶ V$
36	34 35	sylibr	$⊢ (((y \in Fin \land \neg z \in y) \land z = \emptyset) \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to (f \cup \{⟨z, w⟩\}) Fn (y \cup \{z\})$
37		simplr	$⊢ (((y \in Fin \land \neg z \in y) \land z = \emptyset) \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to z = \emptyset$
38		simprr	$⊢ (((y \in Fin \land \neg z \in y) \land z = \emptyset) \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to \forall x \in y (x \neq \emptyset \to f (x) \in x)$
39		nfv	$⊢ Ⅎ x (z = \emptyset \land \neg z \in y)$
40		nfra1	$⊢ Ⅎ x \forall x \in y (x \neq \emptyset \to f (x) \in x)$
41	39 40	nfan	$⊢ Ⅎ x ((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x))$
42		simpr	$⊢ (((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to x \in y$
43		simpllr	$⊢ (((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \to \neg z \in y$
44	43	adantr	$⊢ ((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \to \neg z \in y$
45	44	adantr	$⊢ (((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to \neg z \in y$
46	42 45	jca	$⊢ (((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to (x \in y \land \neg z \in y)$
47		nelne2	$⊢ (x \in y \land \neg z \in y) \to x \neq z$
48	47	necomd	$⊢ (x \in y \land \neg z \in y) \to z \neq x$
49	46 48	syl	$⊢ (((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to z \neq x$
50		fvunsn	$⊢ z \neq x \to (f \cup \{⟨z, w⟩\}) (x) = f (x)$
51	49 50	syl	$⊢ (((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to (f \cup \{⟨z, w⟩\}) (x) = f (x)$
52		simpllr	$⊢ ((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \to \forall x \in y (x \neq \emptyset \to f (x) \in x)$
53	52	adantr	$⊢ (((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to \forall x \in y (x \neq \emptyset \to f (x) \in x)$
54		simplr	$⊢ (((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to x \neq \emptyset$
55		neeq1	$⊢ u = x \to (u \neq \emptyset \leftrightarrow x \neq \emptyset)$
56		fveq2	$⊢ u = x \to f (u) = f (x)$
57	56	eleq1d	$⊢ u = x \to (f (u) \in u \leftrightarrow f (x) \in u)$
58		eleq2w	$⊢ u = x \to (f (x) \in u \leftrightarrow f (x) \in x)$
59	57 58	bitrd	$⊢ u = x \to (f (u) \in u \leftrightarrow f (x) \in x)$
60	55 59	imbi12d	$⊢ u = x \to ((u \neq \emptyset \to f (u) \in u) \leftrightarrow (x \neq \emptyset \to f (x) \in x))$
61	60	cbvralvw	$⊢ \forall u \in y (u \neq \emptyset \to f (u) \in u) \leftrightarrow \forall x \in y (x \neq \emptyset \to f (x) \in x)$
62	60	rspcv	$⊢ x \in y \to (\forall u \in y (u \neq \emptyset \to f (u) \in u) \to (x \neq \emptyset \to f (x) \in x))$
63	61 62	syl5bir	$⊢ x \in y \to (\forall x \in y (x \neq \emptyset \to f (x) \in x) \to (x \neq \emptyset \to f (x) \in x))$
64	42 53 54 63	syl3c	$⊢ (((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to f (x) \in x$
65	51 64	eqeltrd	$⊢ (((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to (f \cup \{⟨z, w⟩\}) (x) \in x$
66		simp-4l	$⊢ ((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \to z = \emptyset$
67	66	adantr	$⊢ (((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to z = \emptyset$
68		simpr	$⊢ (((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to x \in \{z\}$
69		simplr	$⊢ (((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to x \neq \emptyset$
70		elsni	$⊢ x \in \{z\} \to x = z$
71	70	3ad2ant2	$⊢ (z = \emptyset \land x \in \{z\} \land x \neq \emptyset) \to x = z$
72		simp1	$⊢ (z = \emptyset \land x \in \{z\} \land x \neq \emptyset) \to z = \emptyset$
73	71 72	eqtrd	$⊢ (z = \emptyset \land x \in \{z\} \land x \neq \emptyset) \to x = \emptyset$
74		simp3	$⊢ (z = \emptyset \land x \in \{z\} \land x \neq \emptyset) \to x \neq \emptyset$
75	73 74	pm2.21ddne	$⊢ (z = \emptyset \land x \in \{z\} \land x \neq \emptyset) \to (f \cup \{⟨z, w⟩\}) (x) \in x$
76	67 68 69 75	syl3anc	$⊢ (((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to (f \cup \{⟨z, w⟩\}) (x) \in x$
77		simplr	$⊢ ((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \to x \in (y \cup \{z\})$
78		elun	$⊢ x \in (y \cup \{z\}) \leftrightarrow (x \in y \lor x \in \{z\})$
79	77 78	sylib	$⊢ ((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \to (x \in y \lor x \in \{z\})$
80	65 76 79	mpjaodan	$⊢ ((((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \to (f \cup \{⟨z, w⟩\}) (x) \in x$
81	80	ex	$⊢ (((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \land x \in (y \cup \{z\})) \to (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x)$
82	81	ex	$⊢ ((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \to (x \in (y \cup \{z\}) \to (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x))$
83	41 82	ralrimi	$⊢ ((z = \emptyset \land \neg z \in y) \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \to \forall x \in (y \cup \{z\}) (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x)$
84	37 30 38 83	syl21anc	$⊢ (((y \in Fin \land \neg z \in y) \land z = \emptyset) \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to \forall x \in (y \cup \{z\}) (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x)$
85	36 84	jca	$⊢ (((y \in Fin \land \neg z \in y) \land z = \emptyset) \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to ((f \cup \{⟨z, w⟩\}) Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x))$
86	85	ex	$⊢ ((y \in Fin \land \neg z \in y) \land z = \emptyset) \to ((f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \to ((f \cup \{⟨z, w⟩\}) Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x)))$
87	86	eximdv	$⊢ ((y \in Fin \land \neg z \in y) \land z = \emptyset) \to (\exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \to \exists f ((f \cup \{⟨z, w⟩\}) Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x)))$
88		vex	$⊢ f \in V$
89		snex	$⊢ \{⟨z, w⟩\} \in V$
90	88 89	unex	$⊢ f \cup \{⟨z, w⟩\} \in V$
91		fneq1	$⊢ g = f \cup \{⟨z, w⟩\} \to (g Fn (y \cup \{z\}) \leftrightarrow (f \cup \{⟨z, w⟩\}) Fn (y \cup \{z\}))$
92		fveq1	$⊢ g = f \cup \{⟨z, w⟩\} \to g (x) = (f \cup \{⟨z, w⟩\}) (x)$
93	92	eleq1d	$⊢ g = f \cup \{⟨z, w⟩\} \to (g (x) \in x \leftrightarrow (f \cup \{⟨z, w⟩\}) (x) \in x)$
94	93	imbi2d	$⊢ g = f \cup \{⟨z, w⟩\} \to ((x \neq \emptyset \to g (x) \in x) \leftrightarrow (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x))$
95	94	ralbidv	$⊢ g = f \cup \{⟨z, w⟩\} \to (\forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x) \leftrightarrow \forall x \in (y \cup \{z\}) (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x))$
96	91 95	anbi12d	$⊢ g = f \cup \{⟨z, w⟩\} \to ((g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x)) \leftrightarrow ((f \cup \{⟨z, w⟩\}) Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x)))$
97	90 96	spcev	$⊢ ((f \cup \{⟨z, w⟩\}) Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x)) \to \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x))$
98	97	eximi	$⊢ \exists f ((f \cup \{⟨z, w⟩\}) Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x)) \to \exists f \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x))$
99	87 98	syl6	$⊢ ((y \in Fin \land \neg z \in y) \land z = \emptyset) \to (\exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \to \exists f \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x)))$
100		ax5e	$⊢ \exists f \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x)) \to \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x))$
101	99 100	syl6	$⊢ ((y \in Fin \land \neg z \in y) \land z = \emptyset) \to (\exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \to \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x)))$
102	101	imp	$⊢ (((y \in Fin \land \neg z \in y) \land z = \emptyset) \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x))$
103	102	an32s	$⊢ (((y \in Fin \land \neg z \in y) \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \land z = \emptyset) \to \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x))$
104		fneq1	$⊢ f = g \to (f Fn (y \cup \{z\}) \leftrightarrow g Fn (y \cup \{z\}))$
105		fveq1	$⊢ f = g \to f (x) = g (x)$
106	105	eleq1d	$⊢ f = g \to (f (x) \in x \leftrightarrow g (x) \in x)$
107	106	imbi2d	$⊢ f = g \to ((x \neq \emptyset \to f (x) \in x) \leftrightarrow (x \neq \emptyset \to g (x) \in x))$
108	107	ralbidv	$⊢ f = g \to (\forall x \in (y \cup \{z\}) (x \neq \emptyset \to f (x) \in x) \leftrightarrow \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x))$
109	104 108	anbi12d	$⊢ f = g \to ((f Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to f (x) \in x)) \leftrightarrow (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x)))$
110	109	cbvexvw	$⊢ \exists f (f Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to f (x) \in x)) \leftrightarrow \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x))$
111	103 110	sylibr	$⊢ (((y \in Fin \land \neg z \in y) \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \land z = \emptyset) \to \exists f (f Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to f (x) \in x))$
112		simpllr	$⊢ (((y \in Fin \land \neg z \in y) \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \land \neg z = \emptyset) \to \neg z \in y$
113		simpr	$⊢ (((y \in Fin \land \neg z \in y) \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \land \neg z = \emptyset) \to \neg z = \emptyset$
114		neq0	$⊢ \neg z = \emptyset \leftrightarrow \exists w w \in z$
115	113 114	sylib	$⊢ (((y \in Fin \land \neg z \in y) \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \land \neg z = \emptyset) \to \exists w w \in z$
116		simplr	$⊢ (((y \in Fin \land \neg z \in y) \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \land \neg z = \emptyset) \to \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))$
117	115 116	jca	$⊢ (((y \in Fin \land \neg z \in y) \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \land \neg z = \emptyset) \to (\exists w w \in z \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))$
118	112 117	jca	$⊢ (((y \in Fin \land \neg z \in y) \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \land \neg z = \emptyset) \to (\neg z \in y \land (\exists w w \in z \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))))$
119		exdistrv	$⊢ \exists w \exists f (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \leftrightarrow (\exists w w \in z \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))$
120		simprrl	$⊢ (\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to f Fn y$
121	120 25	sylib	$⊢ (\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to f : y ⟶ V$
122	28	a1i	$⊢ (\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to z \in V$
123		simpl	$⊢ (\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to \neg z \in y$
124	31	a1i	$⊢ (\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to w \in V$
125	121 122 123 124 33	syl121anc	$⊢ (\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to (f \cup \{⟨z, w⟩\}) : y \cup \{z\} ⟶ V$
126	125 35	sylibr	$⊢ (\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to (f \cup \{⟨z, w⟩\}) Fn (y \cup \{z\})$
127		nfv	$⊢ Ⅎ x \neg z \in y$
128		nfv	$⊢ Ⅎ x w \in z$
129		nfv	$⊢ Ⅎ x f Fn y$
130	129 40	nfan	$⊢ Ⅎ x (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))$
131	128 130	nfan	$⊢ Ⅎ x (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))$
132	127 131	nfan	$⊢ Ⅎ x (\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))))$
133		simpr	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to x \in y$
134		simp-4l	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to \neg z \in y$
135	133 134	jca	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to (x \in y \land \neg z \in y)$
136	48 50	syl	$⊢ (x \in y \land \neg z \in y) \to (f \cup \{⟨z, w⟩\}) (x) = f (x)$
137	135 136	syl	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to (f \cup \{⟨z, w⟩\}) (x) = f (x)$
138		simprrr	$⊢ (\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to \forall x \in y (x \neq \emptyset \to f (x) \in x)$
139	138	ad5ant12	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to \forall x \in y (x \neq \emptyset \to f (x) \in x)$
140		simplr	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to x \neq \emptyset$
141	133 139 140 63	syl3c	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to f (x) \in x$
142	137 141	eqeltrd	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in y) \to (f \cup \{⟨z, w⟩\}) (x) \in x$
143		simplrl	$⊢ ((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \to w \in z$
144	143	adantr	$⊢ (((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \to w \in z$
145	144	adantr	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to w \in z$
146		simpr	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to x \in \{z\}$
147	146 70	syl	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to x = z$
148		fveq2	$⊢ x = z \to (f \cup \{⟨z, w⟩\}) (x) = (f \cup \{⟨z, w⟩\}) (z)$
149	147 148	syl	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to (f \cup \{⟨z, w⟩\}) (x) = (f \cup \{⟨z, w⟩\}) (z)$
150	28	a1i	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to z \in V$
151	31	a1i	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to w \in V$
152		simp-4l	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to \neg z \in y$
153	120	ad5ant12	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to f Fn y$
154	153	fndmd	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to dom f = y$
155	152 154	neleqtrrd	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to \neg z \in dom f$
156		fsnunfv	$⊢ (z \in V \land w \in V \land \neg z \in dom f) \to (f \cup \{⟨z, w⟩\}) (z) = w$
157	150 151 155 156	syl3anc	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to (f \cup \{⟨z, w⟩\}) (z) = w$
158	149 157	eqtrd	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to (f \cup \{⟨z, w⟩\}) (x) = w$
159	145 158 147	3eltr4d	$⊢ ((((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \land x \in \{z\}) \to (f \cup \{⟨z, w⟩\}) (x) \in x$
160		simplr	$⊢ (((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \to x \in (y \cup \{z\})$
161	160 78	sylib	$⊢ (((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \to (x \in y \lor x \in \{z\})$
162	142 159 161	mpjaodan	$⊢ (((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \land x \neq \emptyset) \to (f \cup \{⟨z, w⟩\}) (x) \in x$
163	162	ex	$⊢ ((\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \land x \in (y \cup \{z\})) \to (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x)$
164	163	ex	$⊢ (\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to (x \in (y \cup \{z\}) \to (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x))$
165	132 164	ralrimi	$⊢ (\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to \forall x \in (y \cup \{z\}) (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x)$
166	126 165	jca	$⊢ (\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to ((f \cup \{⟨z, w⟩\}) Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to (f \cup \{⟨z, w⟩\}) (x) \in x))$
167	166 97	syl	$⊢ (\neg z \in y \land (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x))$
168	167	ex	$⊢ \neg z \in y \to ((w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x)))$
169	168	2eximdv	$⊢ \neg z \in y \to (\exists w \exists f (w \in z \land (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to \exists w \exists f \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x)))$
170	119 169	syl5bir	$⊢ \neg z \in y \to ((\exists w w \in z \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to \exists w \exists f \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x)))$
171	170	imp	$⊢ (\neg z \in y \land (\exists w w \in z \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to \exists w \exists f \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x))$
172	100	exlimiv	$⊢ \exists w \exists f \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x)) \to \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x))$
173	171 172	syl	$⊢ (\neg z \in y \land (\exists w w \in z \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to \exists g (g Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to g (x) \in x))$
174	173 110	sylibr	$⊢ (\neg z \in y \land (\exists w w \in z \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)))) \to \exists f (f Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to f (x) \in x))$
175	118 174	syl	$⊢ (((y \in Fin \land \neg z \in y) \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \land \neg z = \emptyset) \to \exists f (f Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to f (x) \in x))$
176	111 175	pm2.61dan	$⊢ ((y \in Fin \land \neg z \in y) \land \exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x))) \to \exists f (f Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to f (x) \in x))$
177	176	ex	$⊢ (y \in Fin \land \neg z \in y) \to (\exists f (f Fn y \land \forall x \in y (x \neq \emptyset \to f (x) \in x)) \to \exists f (f Fn (y \cup \{z\}) \land \forall x \in (y \cup \{z\}) (x \neq \emptyset \to f (x) \in x)))$
178	4 8 12 16 24 177	findcard2s	$⊢ A \in Fin \to \exists f (f Fn A \land \forall x \in A (x \neq \emptyset \to f (x) \in x))$

Metamath Proof Explorer

Theorem fnchoice

Proof