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

Theorem dfac9 8841
 Description: Equivalence of the axiom of choice with a statement related to ac9 9188; 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 8827 . 2 (CHOICE ↔ ∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
2 vex 3176 . . . . . . 7 𝑓 ∈ V
32rnex 6992 . . . . . 6 ran 𝑓 ∈ V
4 raleq 3115 . . . . . . 7 (𝑠 = ran 𝑓 → (∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) ↔ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)))
54exbidv 1837 . . . . . 6 (𝑠 = ran 𝑓 → (∃𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) ↔ ∃𝑔𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)))
63, 5spcv 3272 . . . . 5 (∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → ∃𝑔𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
7 df-nel 2783 . . . . . . . . . . . . . . 15 (∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ ran 𝑓)
87biimpi 205 . . . . . . . . . . . . . 14 (∅ ∉ ran 𝑓 → ¬ ∅ ∈ ran 𝑓)
98ad2antlr 759 . . . . . . . . . . . . 13 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ¬ ∅ ∈ ran 𝑓)
10 fvelrn 6260 . . . . . . . . . . . . . . . 16 ((Fun 𝑓𝑥 ∈ dom 𝑓) → (𝑓𝑥) ∈ ran 𝑓)
1110adantlr 747 . . . . . . . . . . . . . . 15 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓𝑥) ∈ ran 𝑓)
12 eleq1 2676 . . . . . . . . . . . . . . 15 ((𝑓𝑥) = ∅ → ((𝑓𝑥) ∈ ran 𝑓 ↔ ∅ ∈ ran 𝑓))
1311, 12syl5ibcom 234 . . . . . . . . . . . . . 14 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓𝑥) = ∅ → ∅ ∈ ran 𝑓))
1413necon3bd 2796 . . . . . . . . . . . . 13 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (¬ ∅ ∈ ran 𝑓 → (𝑓𝑥) ≠ ∅))
159, 14mpd 15 . . . . . . . . . . . 12 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓𝑥) ≠ ∅)
1615adantlr 747 . . . . . . . . . . 11 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑓𝑥) ≠ ∅)
17 simpll 786 . . . . . . . . . . . . 13 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) → Fun 𝑓)
1817, 10sylan 487 . . . . . . . . . . . 12 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑓𝑥) ∈ ran 𝑓)
19 simplr 788 . . . . . . . . . . . 12 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
20 neeq1 2844 . . . . . . . . . . . . . 14 (𝑡 = (𝑓𝑥) → (𝑡 ≠ ∅ ↔ (𝑓𝑥) ≠ ∅))
21 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑡 = (𝑓𝑥) → (𝑔𝑡) = (𝑔‘(𝑓𝑥)))
22 id 22 . . . . . . . . . . . . . . 15 (𝑡 = (𝑓𝑥) → 𝑡 = (𝑓𝑥))
2321, 22eleq12d 2682 . . . . . . . . . . . . . 14 (𝑡 = (𝑓𝑥) → ((𝑔𝑡) ∈ 𝑡 ↔ (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥)))
2420, 23imbi12d 333 . . . . . . . . . . . . 13 (𝑡 = (𝑓𝑥) → ((𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) ↔ ((𝑓𝑥) ≠ ∅ → (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥))))
2524rspcva 3280 . . . . . . . . . . . 12 (((𝑓𝑥) ∈ ran 𝑓 ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) → ((𝑓𝑥) ≠ ∅ → (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥)))
2618, 19, 25syl2anc 691 . . . . . . . . . . 11 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓𝑥) ≠ ∅ → (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥)))
2716, 26mpd 15 . . . . . . . . . 10 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥))
2827ralrimiva 2949 . . . . . . . . 9 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) → ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥))
292dmex 6991 . . . . . . . . . 10 dom 𝑓 ∈ V
30 mptelixpg 7831 . . . . . . . . . 10 (dom 𝑓 ∈ V → ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥)))
3129, 30ax-mp 5 . . . . . . . . 9 ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥))
3228, 31sylibr 223 . . . . . . . 8 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) → (𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓𝑥))
33 ne0i 3880 . . . . . . . 8 ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓𝑥) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅)
3432, 33syl 17 . . . . . . 7 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅)
3534ex 449 . . . . . 6 ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
3635exlimdv 1848 . . . . 5 ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∃𝑔𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
376, 36syl5com 31 . . . 4 (∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
3837alrimiv 1842 . . 3 (∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
39 fnresi 5922 . . . . . . 7 ( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅})
40 fnfun 5902 . . . . . . 7 (( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅}) → Fun ( I ↾ (𝑠 ∖ {∅})))
4139, 40ax-mp 5 . . . . . 6 Fun ( I ↾ (𝑠 ∖ {∅}))
42 neldifsn 4262 . . . . . 6 ¬ ∅ ∈ (𝑠 ∖ {∅})
43 vex 3176 . . . . . . . . 9 𝑠 ∈ V
44 difexg 4735 . . . . . . . . 9 (𝑠 ∈ V → (𝑠 ∖ {∅}) ∈ V)
4543, 44ax-mp 5 . . . . . . . 8 (𝑠 ∖ {∅}) ∈ V
46 resiexg 6994 . . . . . . . 8 ((𝑠 ∖ {∅}) ∈ V → ( I ↾ (𝑠 ∖ {∅})) ∈ V)
4745, 46ax-mp 5 . . . . . . 7 ( I ↾ (𝑠 ∖ {∅})) ∈ V
48 funeq 5823 . . . . . . . . 9 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (Fun 𝑓 ↔ Fun ( I ↾ (𝑠 ∖ {∅}))))
49 rneq 5272 . . . . . . . . . . . . 13 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = ran ( I ↾ (𝑠 ∖ {∅})))
50 rnresi 5398 . . . . . . . . . . . . 13 ran ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
5149, 50syl6eq 2660 . . . . . . . . . . . 12 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = (𝑠 ∖ {∅}))
5251eleq2d 2673 . . . . . . . . . . 11 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (∅ ∈ ran 𝑓 ↔ ∅ ∈ (𝑠 ∖ {∅})))
5352notbid 307 . . . . . . . . . 10 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (¬ ∅ ∈ ran 𝑓 ↔ ¬ ∅ ∈ (𝑠 ∖ {∅})))
547, 53syl5bb 271 . . . . . . . . 9 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ (𝑠 ∖ {∅})))
5548, 54anbi12d 743 . . . . . . . 8 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ↔ (Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅}))))
56 dmeq 5246 . . . . . . . . . . . 12 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = dom ( I ↾ (𝑠 ∖ {∅})))
57 dmresi 5376 . . . . . . . . . . . 12 dom ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
5856, 57syl6eq 2660 . . . . . . . . . . 11 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = (𝑠 ∖ {∅}))
5958ixpeq1d 7806 . . . . . . . . . 10 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})(𝑓𝑥))
60 fveq1 6102 . . . . . . . . . . . 12 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (𝑓𝑥) = (( I ↾ (𝑠 ∖ {∅}))‘𝑥))
61 fvresi 6344 . . . . . . . . . . . 12 (𝑥 ∈ (𝑠 ∖ {∅}) → (( I ↾ (𝑠 ∖ {∅}))‘𝑥) = 𝑥)
6260, 61sylan9eq 2664 . . . . . . . . . . 11 ((𝑓 = ( I ↾ (𝑠 ∖ {∅})) ∧ 𝑥 ∈ (𝑠 ∖ {∅})) → (𝑓𝑥) = 𝑥)
6362ixpeq2dva 7809 . . . . . . . . . 10 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})(𝑓𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
6459, 63eqtrd 2644 . . . . . . . . 9 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
6564neeq1d 2841 . . . . . . . 8 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅ ↔ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
6655, 65imbi12d 333 . . . . . . 7 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) ↔ ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)))
6747, 66spcv 3272 . . . . . 6 (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) → ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
6841, 42, 67mp2ani 710 . . . . 5 (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)
69 n0 3890 . . . . . 6 (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ ↔ ∃𝑔 𝑔X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
70 vex 3176 . . . . . . . . 9 𝑔 ∈ V
7170elixp 7801 . . . . . . . 8 (𝑔X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ↔ (𝑔 Fn (𝑠 ∖ {∅}) ∧ ∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥))
72 eldifsn 4260 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑠 ∖ {∅}) ↔ (𝑥𝑠𝑥 ≠ ∅))
7372imbi1i 338 . . . . . . . . . . . . 13 ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔𝑥) ∈ 𝑥) ↔ ((𝑥𝑠𝑥 ≠ ∅) → (𝑔𝑥) ∈ 𝑥))
74 impexp 461 . . . . . . . . . . . . 13 (((𝑥𝑠𝑥 ≠ ∅) → (𝑔𝑥) ∈ 𝑥) ↔ (𝑥𝑠 → (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
7573, 74bitri 263 . . . . . . . . . . . 12 ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔𝑥) ∈ 𝑥) ↔ (𝑥𝑠 → (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
7675ralbii2 2961 . . . . . . . . . . 11 (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥 ↔ ∀𝑥𝑠 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))
77 neeq1 2844 . . . . . . . . . . . . 13 (𝑥 = 𝑡 → (𝑥 ≠ ∅ ↔ 𝑡 ≠ ∅))
78 fveq2 6103 . . . . . . . . . . . . . 14 (𝑥 = 𝑡 → (𝑔𝑥) = (𝑔𝑡))
79 id 22 . . . . . . . . . . . . . 14 (𝑥 = 𝑡𝑥 = 𝑡)
8078, 79eleq12d 2682 . . . . . . . . . . . . 13 (𝑥 = 𝑡 → ((𝑔𝑥) ∈ 𝑥 ↔ (𝑔𝑡) ∈ 𝑡))
8177, 80imbi12d 333 . . . . . . . . . . . 12 (𝑥 = 𝑡 → ((𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)))
8281cbvralv 3147 . . . . . . . . . . 11 (∀𝑥𝑠 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8376, 82bitri 263 . . . . . . . . . 10 (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥 ↔ ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8483biimpi 205 . . . . . . . . 9 (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥 → ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8584adantl 481 . . . . . . . 8 ((𝑔 Fn (𝑠 ∖ {∅}) ∧ ∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥) → ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8671, 85sylbi 206 . . . . . . 7 (𝑔X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8786eximi 1752 . . . . . 6 (∃𝑔 𝑔X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∃𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8869, 87sylbi 206 . . . . 5 (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ → ∃𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8968, 88syl 17 . . . 4 (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) → ∃𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
9089alrimiv 1842 . . 3 (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) → ∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
9138, 90impbii 198 . 2 (∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
921, 91bitri 263 1 (CHOICE ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780   ∉ wnel 2781  ∀wral 2896  Vcvv 3173   ∖ cdif 3537  ∅c0 3874  {csn 4125   ↦ cmpt 4643   I cid 4948  dom cdm 5038  ran crn 5039   ↾ cres 5040  Fun wfun 5798   Fn wfn 5799  ‘cfv 5804  Xcixp 7794  CHOICEwac 8821 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ixp 7795  df-ac 8822 This theorem is referenced by:  dfac14  21231  dfac21  36654
 Copyright terms: Public domain W3C validator