Theorem dfac9 10136

Description: Equivalence of the axiom of choice with a statement related to ac9 10482; 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 10121	. 2 ⊢ (CHOICE ↔ ∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
2		vex 3461	. . . . . . 7 ⊢ 𝑓 ∈ V
3	2	rnex 7913	. . . . . 6 ⊢ ran 𝑓 ∈ V
4		raleq 3322	. . . . . . 7 ⊢ (𝑠 = ran 𝑓 → (∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)))
5	4	exbidv 1954	. . . . . 6 ⊢ (𝑠 = ran 𝑓 → (∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)))
6	3, 5	spcv 3566	. . . . 5 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
7		df-nel 3067	. . . . . . . . . . . . . . 15 ⊢ (∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ ran 𝑓)
8	7	biimpi 219	. . . . . . . . . . . . . 14 ⊢ (∅ ∉ ran 𝑓 → ¬ ∅ ∈ ran 𝑓)
9	8	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ¬ ∅ ∈ ran 𝑓)
10		fvelrn 7075	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑓 ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓)
11	10	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓)
12		eleq1 2853	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑥) = ∅ → ((𝑓‘𝑥) ∈ ran 𝑓 ↔ ∅ ∈ ran 𝑓))
13	11, 12	syl5ibcom 248	. . . . . . . . . . . . . 14 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓‘𝑥) = ∅ → ∅ ∈ ran 𝑓))
14	13	necon3bd 2974	. . . . . . . . . . . . 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 3022	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑓‘𝑥) → (𝑡 ≠ ∅ ↔ (𝑓‘𝑥) ≠ ∅))
18		fveq2 6885	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑓‘𝑥) → (𝑔‘𝑡) = (𝑔‘(𝑓‘𝑥)))
19		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑓‘𝑥) → 𝑡 = (𝑓‘𝑥))
20	18, 19	eleq12d 2859	. . . . . . . . . . . . 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 3584	. . . . . . . . . . 11 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓‘𝑥) ≠ ∅ → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)))
25	16, 24	mpd 16	. . . . . . . . . 10 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))
26	25	ralrimiva 3159	. . . . . . . . 9 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))
27	2	dmex 7912	. . . . . . . . . 10 ⊢ dom 𝑓 ∈ V
28		mptelixpg 8939	. . . . . . . . . 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 4295	. . . . . . 7 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅)
32	31	ex 418	. . . . . 6 ⊢ ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
33	32	exlimdv 1966	. . . . 5 ⊢ ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
34	6, 33	syl5com 32	. . . 4 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
35	34	alrimiv 1960	. . 3 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
36		fnresi 6668	. . . . . . 7 ⊢ ( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅})
37		fnfun 6639	. . . . . . 7 ⊢ (( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅}) → Fun ( I ↾ (𝑠 ∖ {∅})))
38	36, 37	ax-mp 5	. . . . . 6 ⊢ Fun ( I ↾ (𝑠 ∖ {∅}))
39		neldifsn 4762	. . . . . 6 ⊢ ¬ ∅ ∈ (𝑠 ∖ {∅})
40		vex 3461	. . . . . . . . 9 ⊢ 𝑠 ∈ V
41	40	difexi 5303	. . . . . . . 8 ⊢ (𝑠 ∖ {∅}) ∈ V
42		resiexg 7915	. . . . . . . 8 ⊢ ((𝑠 ∖ {∅}) ∈ V → ( I ↾ (𝑠 ∖ {∅})) ∈ V)
43	41, 42	ax-mp 5	. . . . . . 7 ⊢ ( I ↾ (𝑠 ∖ {∅})) ∈ V
44		funeq 6560	. . . . . . . . 9 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (Fun 𝑓 ↔ Fun ( I ↾ (𝑠 ∖ {∅}))))
45		rneq 5928	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = ran ( I ↾ (𝑠 ∖ {∅})))
46		rnresi 6079	. . . . . . . . . . . . 13 ⊢ ran ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
47	45, 46	eqtrdi 2816	. . . . . . . . . . . 12 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = (𝑠 ∖ {∅}))
48	47	eleq2d 2851	. . . . . . . . . . 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 5895	. . . . . . . . . . . 12 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = dom ( I ↾ (𝑠 ∖ {∅})))
53		dmresi 6056	. . . . . . . . . . . 12 ⊢ dom ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
54	52, 53	eqtrdi 2816	. . . . . . . . . . 11 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = (𝑠 ∖ {∅}))
55	54	ixpeq1d 8913	. . . . . . . . . 10 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})(𝑓‘𝑥))
56		fveq1 6884	. . . . . . . . . . . 12 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (𝑓‘𝑥) = (( I ↾ (𝑠 ∖ {∅}))‘𝑥))
57		fvresi 7177	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑠 ∖ {∅}) → (( I ↾ (𝑠 ∖ {∅}))‘𝑥) = 𝑥)
58	56, 57	sylan9eq 2820	. . . . . . . . . . 11 ⊢ ((𝑓 = ( I ↾ (𝑠 ∖ {∅})) ∧ 𝑥 ∈ (𝑠 ∖ {∅})) → (𝑓‘𝑥) = 𝑥)
59	58	ixpeq2dva 8916	. . . . . . . . . 10 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
60	55, 59	eqtrd 2800	. . . . . . . . 9 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
61	60	neeq1d 3019	. . . . . . . 8 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅ ↔ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
62	51, 61	imbi12d 347	. . . . . . 7 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) ↔ ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)))
63	43, 62	spcv 3566	. . . . . 6 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
64	38, 39, 63	mp2ani 711	. . . . 5 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)
65		n0 4307	. . . . . 6 ⊢ (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ ↔ ∃𝑔 𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
66		vex 3461	. . . . . . . . 9 ⊢ 𝑔 ∈ V
67	66	elixp 8908	. . . . . . . 8 ⊢ (𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ↔ (𝑔 Fn (𝑠 ∖ {∅}) ∧ ∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥))
68		eldifsn 4755	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝑠 ∖ {∅}) ↔ (𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅))
69	68	imbi1i 352	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔‘𝑥) ∈ 𝑥) ↔ ((𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅) → (𝑔‘𝑥) ∈ 𝑥))
70		impexp 456	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅) → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ∈ 𝑠 → (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
71	69, 70	bitri 278	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ∈ 𝑠 → (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
72	71	ralbii2 3109	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 ↔ ∀𝑥 ∈ 𝑠 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))
73		neeq1 3022	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑥 ≠ ∅ ↔ 𝑡 ≠ ∅))
74		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡))
75		id 23	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑡 → 𝑥 = 𝑡)
76	74, 75	eleq12d 2859	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → ((𝑔‘𝑥) ∈ 𝑥 ↔ (𝑔‘𝑡) ∈ 𝑡))
77	73, 76	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → ((𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)))
78	77	cbvralvw 3245	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑠 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
79	72, 78	bitri 278	. . . . . . . . 9 ⊢ (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 ↔ ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
80	79	biimpi 219	. . . . . . . 8 ⊢ (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 → ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
81	67, 80	simplbiim 514	. . . . . . 7 ⊢ (𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
82	81	eximi 1868	. . . . . 6 ⊢ (∃𝑔 𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
83	65, 82	sylbi 220	. . . . 5 ⊢ (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
84	64, 83	syl 18	. . . 4 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
85	84	alrimiv 1960	. . 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 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2146   ≠ wne 2960   ∉ wnel 3066  ∀wral 3081  Vcvv 3457   ∖ cdif 3903  ∅c0 4286  {csn 4591   ↦ cmpt 5194   I cid 5557  dom cdm 5663  ran crn 5664   ↾ cres 5665  Fun wfun 6534   Fn wfn 6535  ‘cfv 6540  Xcixp 8901  CHOICEwac 10115

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ixp 8902  df-ac 10116

This theorem is used by:  dfac14  23828  dfac21  43853