Theorem dfac9 10225

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

Assertion

Ref	Expression
dfac9	⊢ (CHOICE ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))

Distinct variable group:   𝑥,𝑓

Proof of Theorem dfac9

Dummy variables 𝑔 𝑠 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfac3 10210	. 2 ⊢ (CHOICE ↔ ∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
2		vex 3457	. . . . . . 7 ⊢ 𝑓 ∈ V
3	2	rnex 7929	. . . . . 6 ⊢ ran 𝑓 ∈ V
4		raleq 3319	. . . . . . 7 ⊢ (𝑠 = ran 𝑓 → (∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)))
5	4	exbidv 1955	. . . . . 6 ⊢ (𝑠 = ran 𝑓 → (∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)))
6	3, 5	spcv 3562	. . . . 5 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
7		df-nel 3065	. . . . . . . . . . . . . . 15 ⊢ (∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ ran 𝑓)
8	7	biimpi 219	. . . . . . . . . . . . . 14 ⊢ (∅ ∉ ran 𝑓 → ¬ ∅ ∈ ran 𝑓)
9	8	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ¬ ∅ ∈ ran 𝑓)
10		fvelrn 7084	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑓 ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓)
11	10	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓)
12		eleq1 2851	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑥) = ∅ → ((𝑓‘𝑥) ∈ ran 𝑓 ↔ ∅ ∈ ran 𝑓))
13	11, 12	syl5ibcom 248	. . . . . . . . . . . . . 14 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓‘𝑥) = ∅ → ∅ ∈ ran 𝑓))
14	13	necon3bd 2972	. . . . . . . . . . . . 13 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (¬ ∅ ∈ ran 𝑓 → (𝑓‘𝑥) ≠ ∅))
15	9, 14	mpd 16	. . . . . . . . . . . 12 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ≠ ∅)
16	15	adantlr 728	. . . . . . . . . . 11 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ≠ ∅)
17		neeq1 3020	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑓‘𝑥) → (𝑡 ≠ ∅ ↔ (𝑓‘𝑥) ≠ ∅))
18		fveq2 6893	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑓‘𝑥) → (𝑔‘𝑡) = (𝑔‘(𝑓‘𝑥)))
19		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑓‘𝑥) → 𝑡 = (𝑓‘𝑥))
20	18, 19	eleq12d 2857	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑓‘𝑥) → ((𝑔‘𝑡) ∈ 𝑡 ↔ (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)))
21	17, 20	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑓‘𝑥) → ((𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ((𝑓‘𝑥) ≠ ∅ → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))))
22		simplr 781	. . . . . . . . . . . 12 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
23	10	ad4ant14 765	. . . . . . . . . . . 12 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓)
24	21, 22, 23	rspcdva 3580	. . . . . . . . . . 11 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓‘𝑥) ≠ ∅ → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)))
25	16, 24	mpd 16	. . . . . . . . . 10 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))
26	25	ralrimiva 3157	. . . . . . . . 9 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))
27	2	dmex 7928	. . . . . . . . . 10 ⊢ dom 𝑓 ∈ V
28		mptelixpg 8974	. . . . . . . . . 10 ⊢ (dom 𝑓 ∈ V → ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓‘𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)))
29	27, 28	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓‘𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))
30	26, 29	sylibr 237	. . . . . . . 8 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → (𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓‘𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓‘𝑥))
31	30	ne0d 4290	. . . . . . 7 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅)
32	31	ex 418	. . . . . 6 ⊢ ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
33	32	exlimdv 1967	. . . . 5 ⊢ ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
34	6, 33	syl5com 32	. . . 4 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
35	34	alrimiv 1961	. . 3 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
36		fnresi 6676	. . . . . . 7 ⊢ ( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅})
37		fnfun 6647	. . . . . . 7 ⊢ (( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅}) → Fun ( I ↾ (𝑠 ∖ {∅})))
38	36, 37	ax-mp 5	. . . . . 6 ⊢ Fun ( I ↾ (𝑠 ∖ {∅}))
39		neldifsn 4754	. . . . . 6 ⊢ ¬ ∅ ∈ (𝑠 ∖ {∅})
40		vex 3457	. . . . . . . . 9 ⊢ 𝑠 ∈ V
41	40	difexi 5295	. . . . . . . 8 ⊢ (𝑠 ∖ {∅}) ∈ V
42		resiexg 7931	. . . . . . . 8 ⊢ ((𝑠 ∖ {∅}) ∈ V → ( I ↾ (𝑠 ∖ {∅})) ∈ V)
43	41, 42	ax-mp 5	. . . . . . 7 ⊢ ( I ↾ (𝑠 ∖ {∅})) ∈ V
44		funeq 6567	. . . . . . . . 9 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (Fun 𝑓 ↔ Fun ( I ↾ (𝑠 ∖ {∅}))))
45		rneq 5922	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = ran ( I ↾ (𝑠 ∖ {∅})))
46		rnresi 6078	. . . . . . . . . . . . 13 ⊢ ran ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
47	45, 46	eqtrdi 2814	. . . . . . . . . . . 12 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = (𝑠 ∖ {∅}))
48	47	eleq2d 2849	. . . . . . . . . . 11 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (∅ ∈ ran 𝑓 ↔ ∅ ∈ (𝑠 ∖ {∅})))
49	48	notbid 321	. . . . . . . . . 10 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (¬ ∅ ∈ ran 𝑓 ↔ ¬ ∅ ∈ (𝑠 ∖ {∅})))
50	7, 49	bitrid 286	. . . . . . . . 9 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ (𝑠 ∖ {∅})))
51	44, 50	anbi12d 644	. . . . . . . 8 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ↔ (Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅}))))
52		dmeq 5889	. . . . . . . . . . . 12 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = dom ( I ↾ (𝑠 ∖ {∅})))
53		dmresi 6049	. . . . . . . . . . . 12 ⊢ dom ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
54	52, 53	eqtrdi 2814	. . . . . . . . . . 11 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = (𝑠 ∖ {∅}))
55	54	ixpeq1d 8948	. . . . . . . . . 10 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})(𝑓‘𝑥))
56		fveq1 6892	. . . . . . . . . . . 12 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (𝑓‘𝑥) = (( I ↾ (𝑠 ∖ {∅}))‘𝑥))
57		fvresi 7185	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑠 ∖ {∅}) → (( I ↾ (𝑠 ∖ {∅}))‘𝑥) = 𝑥)
58	56, 57	sylan9eq 2818	. . . . . . . . . . 11 ⊢ ((𝑓 = ( I ↾ (𝑠 ∖ {∅})) ∧ 𝑥 ∈ (𝑠 ∖ {∅})) → (𝑓‘𝑥) = 𝑥)
59	58	ixpeq2dva 8951	. . . . . . . . . 10 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
60	55, 59	eqtrd 2798	. . . . . . . . 9 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
61	60	neeq1d 3017	. . . . . . . 8 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅ ↔ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
62	51, 61	imbi12d 347	. . . . . . 7 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) ↔ ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)))
63	43, 62	spcv 3562	. . . . . 6 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
64	38, 39, 63	mp2ani 711	. . . . 5 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)
65		n0 4302	. . . . . 6 ⊢ (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ ↔ ∃𝑔 𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
66		vex 3457	. . . . . . . . 9 ⊢ 𝑔 ∈ V
67	66	elixp 8943	. . . . . . . 8 ⊢ (𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ↔ (𝑔 Fn (𝑠 ∖ {∅}) ∧ ∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥))
68		eldifsn 4747	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝑠 ∖ {∅}) ↔ (𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅))
69	68	imbi1i 352	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔‘𝑥) ∈ 𝑥) ↔ ((𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅) → (𝑔‘𝑥) ∈ 𝑥))
70		impexp 456	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅) → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ∈ 𝑠 → (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
71	69, 70	bitri 278	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ∈ 𝑠 → (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
72	71	ralbii2 3107	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 ↔ ∀𝑥 ∈ 𝑠 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))
73		neeq1 3020	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑥 ≠ ∅ ↔ 𝑡 ≠ ∅))
74		fveq2 6893	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡))
75		id 23	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑡 → 𝑥 = 𝑡)
76	74, 75	eleq12d 2857	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → ((𝑔‘𝑥) ∈ 𝑥 ↔ (𝑔‘𝑡) ∈ 𝑡))
77	73, 76	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → ((𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)))
78	77	cbvralvw 3243	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑠 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
79	72, 78	bitri 278	. . . . . . . . 9 ⊢ (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 ↔ ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
80	79	biimpi 219	. . . . . . . 8 ⊢ (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 → ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
81	67, 80	simplbiim 514	. . . . . . 7 ⊢ (𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
82	81	eximi 1867	. . . . . 6 ⊢ (∃𝑔 𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
83	65, 82	sylbi 220	. . . . 5 ⊢ (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
84	64, 83	syl 18	. . . 4 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
85	84	alrimiv 1961	. . 3 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → ∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
86	35, 85	impbii 212	. 2 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
87	1, 86	bitri 278	1 ⊢ (CHOICE ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2146   ≠ wne 2958   ∉ wnel 3064  ∀wral 3079  Vcvv 3453   ∖ cdif 4047  ∅c0 4280  {csn 4587   ↦ cmpt 5188   I cid 5548  dom cdm 5654  ran crn 5655   ↾ cres 5656  Fun wfun 6540   Fn wfn 6541  ‘cfv 6546  Xcixp 8936  CHOICEwac 10204

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5234  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-ixp 8937  df-ac 10205

This theorem is used by:  dfac14  23949  dfac21  44208