MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac9 Structured version   Visualization version   GIF version

Theorem dfac9 8909
Description: Equivalence of the axiom of choice with a statement related to ac9 9256; 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.
StepHypRef Expression
1 dfac3 8895 . 2 (CHOICE ↔ ∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
2 vex 3192 . . . . . . 7 𝑓 ∈ V
32rnex 7054 . . . . . 6 ran 𝑓 ∈ V
4 raleq 3130 . . . . . . 7 (𝑠 = ran 𝑓 → (∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) ↔ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)))
54exbidv 1847 . . . . . 6 (𝑠 = ran 𝑓 → (∃𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) ↔ ∃𝑔𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)))
63, 5spcv 3288 . . . . 5 (∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → ∃𝑔𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
7 df-nel 2894 . . . . . . . . . . . . . . 15 (∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ ran 𝑓)
87biimpi 206 . . . . . . . . . . . . . 14 (∅ ∉ ran 𝑓 → ¬ ∅ ∈ ran 𝑓)
98ad2antlr 762 . . . . . . . . . . . . 13 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ¬ ∅ ∈ ran 𝑓)
10 fvelrn 6313 . . . . . . . . . . . . . . . 16 ((Fun 𝑓𝑥 ∈ dom 𝑓) → (𝑓𝑥) ∈ ran 𝑓)
1110adantlr 750 . . . . . . . . . . . . . . 15 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓𝑥) ∈ ran 𝑓)
12 eleq1 2686 . . . . . . . . . . . . . . 15 ((𝑓𝑥) = ∅ → ((𝑓𝑥) ∈ ran 𝑓 ↔ ∅ ∈ ran 𝑓))
1311, 12syl5ibcom 235 . . . . . . . . . . . . . 14 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓𝑥) = ∅ → ∅ ∈ ran 𝑓))
1413necon3bd 2804 . . . . . . . . . . . . 13 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (¬ ∅ ∈ ran 𝑓 → (𝑓𝑥) ≠ ∅))
159, 14mpd 15 . . . . . . . . . . . 12 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓𝑥) ≠ ∅)
1615adantlr 750 . . . . . . . . . . 11 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑓𝑥) ≠ ∅)
17 simpll 789 . . . . . . . . . . . . 13 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) → Fun 𝑓)
1817, 10sylan 488 . . . . . . . . . . . 12 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑓𝑥) ∈ ran 𝑓)
19 simplr 791 . . . . . . . . . . . 12 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
20 neeq1 2852 . . . . . . . . . . . . . 14 (𝑡 = (𝑓𝑥) → (𝑡 ≠ ∅ ↔ (𝑓𝑥) ≠ ∅))
21 fveq2 6153 . . . . . . . . . . . . . . 15 (𝑡 = (𝑓𝑥) → (𝑔𝑡) = (𝑔‘(𝑓𝑥)))
22 id 22 . . . . . . . . . . . . . . 15 (𝑡 = (𝑓𝑥) → 𝑡 = (𝑓𝑥))
2321, 22eleq12d 2692 . . . . . . . . . . . . . 14 (𝑡 = (𝑓𝑥) → ((𝑔𝑡) ∈ 𝑡 ↔ (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥)))
2420, 23imbi12d 334 . . . . . . . . . . . . 13 (𝑡 = (𝑓𝑥) → ((𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) ↔ ((𝑓𝑥) ≠ ∅ → (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥))))
2524rspcva 3296 . . . . . . . . . . . 12 (((𝑓𝑥) ∈ ran 𝑓 ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) → ((𝑓𝑥) ≠ ∅ → (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥)))
2618, 19, 25syl2anc 692 . . . . . . . . . . 11 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓𝑥) ≠ ∅ → (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥)))
2716, 26mpd 15 . . . . . . . . . 10 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥))
2827ralrimiva 2961 . . . . . . . . 9 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) → ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥))
292dmex 7053 . . . . . . . . . 10 dom 𝑓 ∈ V
30 mptelixpg 7896 . . . . . . . . . 10 (dom 𝑓 ∈ V → ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥)))
3129, 30ax-mp 5 . . . . . . . . 9 ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥))
3228, 31sylibr 224 . . . . . . . 8 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) → (𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓𝑥))
33 ne0i 3902 . . . . . . . 8 ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓𝑥) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅)
3432, 33syl 17 . . . . . . 7 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅)
3534ex 450 . . . . . 6 ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
3635exlimdv 1858 . . . . 5 ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∃𝑔𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
376, 36syl5com 31 . . . 4 (∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
3837alrimiv 1852 . . 3 (∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
39 fnresi 5971 . . . . . . 7 ( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅})
40 fnfun 5951 . . . . . . 7 (( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅}) → Fun ( I ↾ (𝑠 ∖ {∅})))
4139, 40ax-mp 5 . . . . . 6 Fun ( I ↾ (𝑠 ∖ {∅}))
42 neldifsn 4295 . . . . . 6 ¬ ∅ ∈ (𝑠 ∖ {∅})
43 vex 3192 . . . . . . . . 9 𝑠 ∈ V
44 difexg 4773 . . . . . . . . 9 (𝑠 ∈ V → (𝑠 ∖ {∅}) ∈ V)
4543, 44ax-mp 5 . . . . . . . 8 (𝑠 ∖ {∅}) ∈ V
46 resiexg 7056 . . . . . . . 8 ((𝑠 ∖ {∅}) ∈ V → ( I ↾ (𝑠 ∖ {∅})) ∈ V)
4745, 46ax-mp 5 . . . . . . 7 ( I ↾ (𝑠 ∖ {∅})) ∈ V
48 funeq 5872 . . . . . . . . 9 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (Fun 𝑓 ↔ Fun ( I ↾ (𝑠 ∖ {∅}))))
49 rneq 5316 . . . . . . . . . . . . 13 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = ran ( I ↾ (𝑠 ∖ {∅})))
50 rnresi 5443 . . . . . . . . . . . . 13 ran ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
5149, 50syl6eq 2671 . . . . . . . . . . . 12 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = (𝑠 ∖ {∅}))
5251eleq2d 2684 . . . . . . . . . . 11 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (∅ ∈ ran 𝑓 ↔ ∅ ∈ (𝑠 ∖ {∅})))
5352notbid 308 . . . . . . . . . 10 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (¬ ∅ ∈ ran 𝑓 ↔ ¬ ∅ ∈ (𝑠 ∖ {∅})))
547, 53syl5bb 272 . . . . . . . . 9 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ (𝑠 ∖ {∅})))
5548, 54anbi12d 746 . . . . . . . 8 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ↔ (Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅}))))
56 dmeq 5289 . . . . . . . . . . . 12 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = dom ( I ↾ (𝑠 ∖ {∅})))
57 dmresi 5421 . . . . . . . . . . . 12 dom ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
5856, 57syl6eq 2671 . . . . . . . . . . 11 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = (𝑠 ∖ {∅}))
5958ixpeq1d 7871 . . . . . . . . . 10 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})(𝑓𝑥))
60 fveq1 6152 . . . . . . . . . . . 12 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (𝑓𝑥) = (( I ↾ (𝑠 ∖ {∅}))‘𝑥))
61 fvresi 6399 . . . . . . . . . . . 12 (𝑥 ∈ (𝑠 ∖ {∅}) → (( I ↾ (𝑠 ∖ {∅}))‘𝑥) = 𝑥)
6260, 61sylan9eq 2675 . . . . . . . . . . 11 ((𝑓 = ( I ↾ (𝑠 ∖ {∅})) ∧ 𝑥 ∈ (𝑠 ∖ {∅})) → (𝑓𝑥) = 𝑥)
6362ixpeq2dva 7874 . . . . . . . . . 10 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})(𝑓𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
6459, 63eqtrd 2655 . . . . . . . . 9 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
6564neeq1d 2849 . . . . . . . 8 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅ ↔ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
6655, 65imbi12d 334 . . . . . . 7 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) ↔ ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)))
6747, 66spcv 3288 . . . . . 6 (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) → ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
6841, 42, 67mp2ani 713 . . . . 5 (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)
69 n0 3912 . . . . . 6 (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ ↔ ∃𝑔 𝑔X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
70 vex 3192 . . . . . . . . 9 𝑔 ∈ V
7170elixp 7866 . . . . . . . 8 (𝑔X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ↔ (𝑔 Fn (𝑠 ∖ {∅}) ∧ ∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥))
72 eldifsn 4292 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑠 ∖ {∅}) ↔ (𝑥𝑠𝑥 ≠ ∅))
7372imbi1i 339 . . . . . . . . . . . . 13 ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔𝑥) ∈ 𝑥) ↔ ((𝑥𝑠𝑥 ≠ ∅) → (𝑔𝑥) ∈ 𝑥))
74 impexp 462 . . . . . . . . . . . . 13 (((𝑥𝑠𝑥 ≠ ∅) → (𝑔𝑥) ∈ 𝑥) ↔ (𝑥𝑠 → (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
7573, 74bitri 264 . . . . . . . . . . . 12 ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔𝑥) ∈ 𝑥) ↔ (𝑥𝑠 → (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
7675ralbii2 2973 . . . . . . . . . . 11 (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥 ↔ ∀𝑥𝑠 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))
77 neeq1 2852 . . . . . . . . . . . . 13 (𝑥 = 𝑡 → (𝑥 ≠ ∅ ↔ 𝑡 ≠ ∅))
78 fveq2 6153 . . . . . . . . . . . . . 14 (𝑥 = 𝑡 → (𝑔𝑥) = (𝑔𝑡))
79 id 22 . . . . . . . . . . . . . 14 (𝑥 = 𝑡𝑥 = 𝑡)
8078, 79eleq12d 2692 . . . . . . . . . . . . 13 (𝑥 = 𝑡 → ((𝑔𝑥) ∈ 𝑥 ↔ (𝑔𝑡) ∈ 𝑡))
8177, 80imbi12d 334 . . . . . . . . . . . 12 (𝑥 = 𝑡 → ((𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)))
8281cbvralv 3162 . . . . . . . . . . 11 (∀𝑥𝑠 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8376, 82bitri 264 . . . . . . . . . 10 (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥 ↔ ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8483biimpi 206 . . . . . . . . 9 (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥 → ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8584adantl 482 . . . . . . . 8 ((𝑔 Fn (𝑠 ∖ {∅}) ∧ ∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥) → ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8671, 85sylbi 207 . . . . . . 7 (𝑔X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8786eximi 1759 . . . . . 6 (∃𝑔 𝑔X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∃𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8869, 87sylbi 207 . . . . 5 (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ → ∃𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8968, 88syl 17 . . . 4 (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) → ∃𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
9089alrimiv 1852 . . 3 (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) → ∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
9138, 90impbii 199 . 2 (∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
921, 91bitri 264 1 (CHOICE ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wal 1478   = wceq 1480  wex 1701  wcel 1987  wne 2790  wnel 2893  wral 2907  Vcvv 3189  cdif 3556  c0 3896  {csn 4153  cmpt 4678   I cid 4989  dom cdm 5079  ran crn 5080  cres 5081  Fun wfun 5846   Fn wfn 5847  cfv 5852  Xcixp 7859  CHOICEwac 8889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-ixp 7860  df-ac 8890
This theorem is referenced by:  dfac14  21340  dfac21  37143
  Copyright terms: Public domain W3C validator