dfac9

Description: Equivalence of the axiom of choice with a statement related to ac9 ; definition AC3 of Schechter p. 139. (Contributed by Stefan O'Rear, 22-Feb-2015)

		Ref	Expression
	Assertion	dfac9	$⊢ CHOICE \leftrightarrow \forall f ((Fun f \land \emptyset \notin ran f) \to \underset{x \in dom f}{⨉} f (x) \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		dfac3	$⊢ CHOICE \leftrightarrow \forall s \exists g \forall t \in s (t \neq \emptyset \to g (t) \in t)$
2		vex	$⊢ f \in V$
3	2	rnex	$⊢ ran f \in V$
4		raleq	$⊢ s = ran f \to (\forall t \in s (t \neq \emptyset \to g (t) \in t) \leftrightarrow \forall t \in ran f (t \neq \emptyset \to g (t) \in t))$
5	4	exbidv	$⊢ s = ran f \to (\exists g \forall t \in s (t \neq \emptyset \to g (t) \in t) \leftrightarrow \exists g \forall t \in ran f (t \neq \emptyset \to g (t) \in t))$
6	3 5	spcv	$⊢ \forall s \exists g \forall t \in s (t \neq \emptyset \to g (t) \in t) \to \exists g \forall t \in ran f (t \neq \emptyset \to g (t) \in t)$
7		df-nel	$⊢ \emptyset \notin ran f \leftrightarrow \neg \emptyset \in ran f$
8	7	biimpi	$⊢ \emptyset \notin ran f \to \neg \emptyset \in ran f$
9	8	ad2antlr	$⊢ ((Fun f \land \emptyset \notin ran f) \land x \in dom f) \to \neg \emptyset \in ran f$
10		fvelrn	$⊢ (Fun f \land x \in dom f) \to f (x) \in ran f$
11	10	adantlr	$⊢ ((Fun f \land \emptyset \notin ran f) \land x \in dom f) \to f (x) \in ran f$
12		eleq1	$⊢ f (x) = \emptyset \to (f (x) \in ran f \leftrightarrow \emptyset \in ran f)$
13	11 12	syl5ibcom	$⊢ ((Fun f \land \emptyset \notin ran f) \land x \in dom f) \to (f (x) = \emptyset \to \emptyset \in ran f)$
14	13	necon3bd	$⊢ ((Fun f \land \emptyset \notin ran f) \land x \in dom f) \to (\neg \emptyset \in ran f \to f (x) \neq \emptyset)$
15	9 14	mpd	$⊢ ((Fun f \land \emptyset \notin ran f) \land x \in dom f) \to f (x) \neq \emptyset$
16	15	adantlr	$⊢ (((Fun f \land \emptyset \notin ran f) \land \forall t \in ran f (t \neq \emptyset \to g (t) \in t)) \land x \in dom f) \to f (x) \neq \emptyset$
17		neeq1	$⊢ t = f (x) \to (t \neq \emptyset \leftrightarrow f (x) \neq \emptyset)$
18		fveq2	$⊢ t = f (x) \to g (t) = g (f (x))$
19		id	$⊢ t = f (x) \to t = f (x)$
20	18 19	eleq12d	$⊢ t = f (x) \to (g (t) \in t \leftrightarrow g (f (x)) \in f (x))$
21	17 20	imbi12d	$⊢ t = f (x) \to ((t \neq \emptyset \to g (t) \in t) \leftrightarrow (f (x) \neq \emptyset \to g (f (x)) \in f (x)))$
22		simplr	$⊢ (((Fun f \land \emptyset \notin ran f) \land \forall t \in ran f (t \neq \emptyset \to g (t) \in t)) \land x \in dom f) \to \forall t \in ran f (t \neq \emptyset \to g (t) \in t)$
23	10	ad4ant14	$⊢ (((Fun f \land \emptyset \notin ran f) \land \forall t \in ran f (t \neq \emptyset \to g (t) \in t)) \land x \in dom f) \to f (x) \in ran f$
24	21 22 23	rspcdva	$⊢ (((Fun f \land \emptyset \notin ran f) \land \forall t \in ran f (t \neq \emptyset \to g (t) \in t)) \land x \in dom f) \to (f (x) \neq \emptyset \to g (f (x)) \in f (x))$
25	16 24	mpd	$⊢ (((Fun f \land \emptyset \notin ran f) \land \forall t \in ran f (t \neq \emptyset \to g (t) \in t)) \land x \in dom f) \to g (f (x)) \in f (x)$
26	25	ralrimiva	$⊢ ((Fun f \land \emptyset \notin ran f) \land \forall t \in ran f (t \neq \emptyset \to g (t) \in t)) \to \forall x \in dom f g (f (x)) \in f (x)$
27	2	dmex	$⊢ dom f \in V$
28		mptelixpg	$⊢ dom f \in V \to ((x \in dom f ⟼ g (f (x))) \in \underset{x \in dom f}{⨉} f (x) \leftrightarrow \forall x \in dom f g (f (x)) \in f (x))$
29	27 28	ax-mp	$⊢ (x \in dom f ⟼ g (f (x))) \in \underset{x \in dom f}{⨉} f (x) \leftrightarrow \forall x \in dom f g (f (x)) \in f (x)$
30	26 29	sylibr	$⊢ ((Fun f \land \emptyset \notin ran f) \land \forall t \in ran f (t \neq \emptyset \to g (t) \in t)) \to (x \in dom f ⟼ g (f (x))) \in \underset{x \in dom f}{⨉} f (x)$
31	30	ne0d	$⊢ ((Fun f \land \emptyset \notin ran f) \land \forall t \in ran f (t \neq \emptyset \to g (t) \in t)) \to \underset{x \in dom f}{⨉} f (x) \neq \emptyset$
32	31	ex	$⊢ (Fun f \land \emptyset \notin ran f) \to (\forall t \in ran f (t \neq \emptyset \to g (t) \in t) \to \underset{x \in dom f}{⨉} f (x) \neq \emptyset)$
33	32	exlimdv	$⊢ (Fun f \land \emptyset \notin ran f) \to (\exists g \forall t \in ran f (t \neq \emptyset \to g (t) \in t) \to \underset{x \in dom f}{⨉} f (x) \neq \emptyset)$
34	6 33	syl5com	$⊢ \forall s \exists g \forall t \in s (t \neq \emptyset \to g (t) \in t) \to ((Fun f \land \emptyset \notin ran f) \to \underset{x \in dom f}{⨉} f (x) \neq \emptyset)$
35	34	alrimiv	$⊢ \forall s \exists g \forall t \in s (t \neq \emptyset \to g (t) \in t) \to \forall f ((Fun f \land \emptyset \notin ran f) \to \underset{x \in dom f}{⨉} f (x) \neq \emptyset)$
36		fnresi	$⊢ ({I ↾}_{(s ∖ \{\emptyset\})}) Fn (s ∖ \{\emptyset\})$
37		fnfun	$⊢ ({I ↾}_{(s ∖ \{\emptyset\})}) Fn (s ∖ \{\emptyset\}) \to Fun ({I ↾}_{(s ∖ \{\emptyset\})})$
38	36 37	ax-mp	$⊢ Fun ({I ↾}_{(s ∖ \{\emptyset\})})$
39		neldifsn	$⊢ \neg \emptyset \in (s ∖ \{\emptyset\})$
40		vex	$⊢ s \in V$
41	40	difexi	$⊢ s ∖ \{\emptyset\} \in V$
42		resiexg	$⊢ s ∖ \{\emptyset\} \in V \to {I ↾}_{(s ∖ \{\emptyset\})} \in V$
43	41 42	ax-mp	$⊢ {I ↾}_{(s ∖ \{\emptyset\})} \in V$
44		funeq	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to (Fun f \leftrightarrow Fun ({I ↾}_{(s ∖ \{\emptyset\})}))$
45		rneq	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to ran f = ran ({I ↾}_{(s ∖ \{\emptyset\})})$
46		rnresi	$⊢ ran ({I ↾}_{(s ∖ \{\emptyset\})}) = s ∖ \{\emptyset\}$
47	45 46	eqtrdi	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to ran f = s ∖ \{\emptyset\}$
48	47	eleq2d	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to (\emptyset \in ran f \leftrightarrow \emptyset \in (s ∖ \{\emptyset\}))$
49	48	notbid	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to (\neg \emptyset \in ran f \leftrightarrow \neg \emptyset \in (s ∖ \{\emptyset\}))$
50	7 49	bitrid	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to (\emptyset \notin ran f \leftrightarrow \neg \emptyset \in (s ∖ \{\emptyset\}))$
51	44 50	anbi12d	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to ((Fun f \land \emptyset \notin ran f) \leftrightarrow (Fun ({I ↾}_{(s ∖ \{\emptyset\})}) \land \neg \emptyset \in (s ∖ \{\emptyset\})))$
52		dmeq	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to dom f = dom ({I ↾}_{(s ∖ \{\emptyset\})})$
53		dmresi	$⊢ dom ({I ↾}_{(s ∖ \{\emptyset\})}) = s ∖ \{\emptyset\}$
54	52 53	eqtrdi	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to dom f = s ∖ \{\emptyset\}$
55	54	ixpeq1d	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to \underset{x \in dom f}{⨉} f (x) = \underset{x \in s ∖ \{\emptyset\}}{⨉} f (x)$
56		fveq1	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to f (x) = ({I ↾}_{(s ∖ \{\emptyset\})}) (x)$
57		fvresi	$⊢ x \in (s ∖ \{\emptyset\}) \to ({I ↾}_{(s ∖ \{\emptyset\})}) (x) = x$
58	56 57	sylan9eq	$⊢ (f = {I ↾}_{(s ∖ \{\emptyset\})} \land x \in (s ∖ \{\emptyset\})) \to f (x) = x$
59	58	ixpeq2dva	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to \underset{x \in s ∖ \{\emptyset\}}{⨉} f (x) = \underset{x \in s ∖ \{\emptyset\}}{⨉} x$
60	55 59	eqtrd	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to \underset{x \in dom f}{⨉} f (x) = \underset{x \in s ∖ \{\emptyset\}}{⨉} x$
61	60	neeq1d	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to (\underset{x \in dom f}{⨉} f (x) \neq \emptyset \leftrightarrow \underset{x \in s ∖ \{\emptyset\}}{⨉} x \neq \emptyset)$
62	51 61	imbi12d	$⊢ f = {I ↾}_{(s ∖ \{\emptyset\})} \to (((Fun f \land \emptyset \notin ran f) \to \underset{x \in dom f}{⨉} f (x) \neq \emptyset) \leftrightarrow ((Fun ({I ↾}_{(s ∖ \{\emptyset\})}) \land \neg \emptyset \in (s ∖ \{\emptyset\})) \to \underset{x \in s ∖ \{\emptyset\}}{⨉} x \neq \emptyset))$
63	43 62	spcv	$⊢ \forall f ((Fun f \land \emptyset \notin ran f) \to \underset{x \in dom f}{⨉} f (x) \neq \emptyset) \to ((Fun ({I ↾}_{(s ∖ \{\emptyset\})}) \land \neg \emptyset \in (s ∖ \{\emptyset\})) \to \underset{x \in s ∖ \{\emptyset\}}{⨉} x \neq \emptyset)$
64	38 39 63	mp2ani	$⊢ \forall f ((Fun f \land \emptyset \notin ran f) \to \underset{x \in dom f}{⨉} f (x) \neq \emptyset) \to \underset{x \in s ∖ \{\emptyset\}}{⨉} x \neq \emptyset$
65		n0	$⊢ \underset{x \in s ∖ \{\emptyset\}}{⨉} x \neq \emptyset \leftrightarrow \exists g g \in \underset{x \in s ∖ \{\emptyset\}}{⨉} x$
66		vex	$⊢ g \in V$
67	66	elixp	$⊢ g \in \underset{x \in s ∖ \{\emptyset\}}{⨉} x \leftrightarrow (g Fn (s ∖ \{\emptyset\}) \land \forall x \in (s ∖ \{\emptyset\}) g (x) \in x)$
68		eldifsn	$⊢ x \in (s ∖ \{\emptyset\}) \leftrightarrow (x \in s \land x \neq \emptyset)$
69	68	imbi1i	$⊢ (x \in (s ∖ \{\emptyset\}) \to g (x) \in x) \leftrightarrow ((x \in s \land x \neq \emptyset) \to g (x) \in x)$
70		impexp	$⊢ ((x \in s \land x \neq \emptyset) \to g (x) \in x) \leftrightarrow (x \in s \to (x \neq \emptyset \to g (x) \in x))$
71	69 70	bitri	$⊢ (x \in (s ∖ \{\emptyset\}) \to g (x) \in x) \leftrightarrow (x \in s \to (x \neq \emptyset \to g (x) \in x))$
72	71	ralbii2	$⊢ \forall x \in (s ∖ \{\emptyset\}) g (x) \in x \leftrightarrow \forall x \in s (x \neq \emptyset \to g (x) \in x)$
73		neeq1	$⊢ x = t \to (x \neq \emptyset \leftrightarrow t \neq \emptyset)$
74		fveq2	$⊢ x = t \to g (x) = g (t)$
75		id	$⊢ x = t \to x = t$
76	74 75	eleq12d	$⊢ x = t \to (g (x) \in x \leftrightarrow g (t) \in t)$
77	73 76	imbi12d	$⊢ x = t \to ((x \neq \emptyset \to g (x) \in x) \leftrightarrow (t \neq \emptyset \to g (t) \in t))$
78	77	cbvralvw	$⊢ \forall x \in s (x \neq \emptyset \to g (x) \in x) \leftrightarrow \forall t \in s (t \neq \emptyset \to g (t) \in t)$
79	72 78	bitri	$⊢ \forall x \in (s ∖ \{\emptyset\}) g (x) \in x \leftrightarrow \forall t \in s (t \neq \emptyset \to g (t) \in t)$
80	79	biimpi	$⊢ \forall x \in (s ∖ \{\emptyset\}) g (x) \in x \to \forall t \in s (t \neq \emptyset \to g (t) \in t)$
81	67 80	simplbiim	$⊢ g \in \underset{x \in s ∖ \{\emptyset\}}{⨉} x \to \forall t \in s (t \neq \emptyset \to g (t) \in t)$
82	81	eximi	$⊢ \exists g g \in \underset{x \in s ∖ \{\emptyset\}}{⨉} x \to \exists g \forall t \in s (t \neq \emptyset \to g (t) \in t)$
83	65 82	sylbi	$⊢ \underset{x \in s ∖ \{\emptyset\}}{⨉} x \neq \emptyset \to \exists g \forall t \in s (t \neq \emptyset \to g (t) \in t)$
84	64 83	syl	$⊢ \forall f ((Fun f \land \emptyset \notin ran f) \to \underset{x \in dom f}{⨉} f (x) \neq \emptyset) \to \exists g \forall t \in s (t \neq \emptyset \to g (t) \in t)$
85	84	alrimiv	$⊢ \forall f ((Fun f \land \emptyset \notin ran f) \to \underset{x \in dom f}{⨉} f (x) \neq \emptyset) \to \forall s \exists g \forall t \in s (t \neq \emptyset \to g (t) \in t)$
86	35 85	impbii	$⊢ \forall s \exists g \forall t \in s (t \neq \emptyset \to g (t) \in t) \leftrightarrow \forall f ((Fun f \land \emptyset \notin ran f) \to \underset{x \in dom f}{⨉} f (x) \neq \emptyset)$
87	1 86	bitri	$⊢ CHOICE \leftrightarrow \forall f ((Fun f \land \emptyset \notin ran f) \to \underset{x \in dom f}{⨉} f (x) \neq \emptyset)$

Metamath Proof Explorer

Theorem dfac9

Proof