Step | Hyp | Ref
| Expression |
1 | | dfac3 8827 |
. 2
⊢
(CHOICE ↔ ∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) |
2 | | vex 3176 |
. . . . . . 7
⊢ 𝑓 ∈ V |
3 | 2 | rnex 6992 |
. . . . . 6
⊢ ran 𝑓 ∈ V |
4 | | raleq 3115 |
. . . . . . 7
⊢ (𝑠 = ran 𝑓 → (∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))) |
5 | 4 | exbidv 1837 |
. . . . . 6
⊢ (𝑠 = ran 𝑓 → (∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))) |
6 | 3, 5 | spcv 3272 |
. . . . 5
⊢
(∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) |
7 | | df-nel 2783 |
. . . . . . . . . . . . . . 15
⊢ (∅
∉ ran 𝑓 ↔ ¬
∅ ∈ ran 𝑓) |
8 | 7 | biimpi 205 |
. . . . . . . . . . . . . 14
⊢ (∅
∉ ran 𝑓 → ¬
∅ ∈ ran 𝑓) |
9 | 8 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ (((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) ∧ 𝑥 ∈ dom 𝑓) → ¬ ∅ ∈ ran 𝑓) |
10 | | fvelrn 6260 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝑓 ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓) |
11 | 10 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓) |
12 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑥) = ∅ → ((𝑓‘𝑥) ∈ ran 𝑓 ↔ ∅ ∈ ran 𝑓)) |
13 | 11, 12 | syl5ibcom 234 |
. . . . . . . . . . . . . 14
⊢ (((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓‘𝑥) = ∅ → ∅ ∈ ran 𝑓)) |
14 | 13 | necon3bd 2796 |
. . . . . . . . . . . . 13
⊢ (((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) ∧ 𝑥 ∈ dom 𝑓) → (¬ ∅ ∈ ran 𝑓 → (𝑓‘𝑥) ≠ ∅)) |
15 | 9, 14 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ≠ ∅) |
16 | 15 | adantlr 747 |
. . . . . . . . . . 11
⊢ ((((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ≠ ∅) |
17 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → Fun 𝑓) |
18 | 17, 10 | sylan 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
⊢ (𝑡 = (𝑓‘𝑥) → 𝑡 = (𝑓‘𝑥)) |
23 | 21, 22 | eleq12d 2682 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (𝑓‘𝑥) → ((𝑔‘𝑡) ∈ 𝑡 ↔ (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))) |
24 | 20, 23 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (𝑓‘𝑥) → ((𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ((𝑓‘𝑥) ≠ ∅ → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)))) |
25 | 24 | rspcva 3280 |
. . . . . . . . . . . 12
⊢ (((𝑓‘𝑥) ∈ ran 𝑓 ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → ((𝑓‘𝑥) ≠ ∅ → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))) |
26 | 18, 19, 25 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓‘𝑥) ≠ ∅ → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))) |
27 | 16, 26 | mpd 15 |
. . . . . . . . . 10
⊢ ((((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)) |
28 | 27 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)) |
29 | 2 | dmex 6991 |
. . . . . . . . . 10
⊢ dom 𝑓 ∈ V |
30 | | mptelixpg 7831 |
. . . . . . . . . 10
⊢ (dom
𝑓 ∈ V → ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓‘𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓‘𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)) |
32 | 28, 31 | sylibr 223 |
. . . . . . . 8
⊢ (((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → (𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓‘𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓‘𝑥)) |
33 | | ne0i 3880 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓‘𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓‘𝑥) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) |
34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ (((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) |
35 | 34 | ex 449 |
. . . . . 6
⊢ ((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) → (∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅)) |
36 | 35 | exlimdv 1848 |
. . . . 5
⊢ ((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) → (∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅)) |
37 | 6, 36 | syl5com 31 |
. . . 4
⊢
(∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅)) |
38 | 37 | alrimiv 1842 |
. . 3
⊢
(∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅)) |
39 | | fnresi 5922 |
. . . . . . 7
⊢ ( I
↾ (𝑠 ∖
{∅})) Fn (𝑠 ∖
{∅}) |
40 | | fnfun 5902 |
. . . . . . 7
⊢ (( I
↾ (𝑠 ∖
{∅})) Fn (𝑠 ∖
{∅}) → Fun ( I ↾ (𝑠 ∖ {∅}))) |
41 | 39, 40 | ax-mp 5 |
. . . . . 6
⊢ Fun ( I
↾ (𝑠 ∖
{∅})) |
42 | | neldifsn 4262 |
. . . . . 6
⊢ ¬
∅ ∈ (𝑠 ∖
{∅}) |
43 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑠 ∈ V |
44 | | difexg 4735 |
. . . . . . . . 9
⊢ (𝑠 ∈ V → (𝑠 ∖ {∅}) ∈
V) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑠 ∖ {∅}) ∈
V |
46 | | resiexg 6994 |
. . . . . . . 8
⊢ ((𝑠 ∖ {∅}) ∈ V
→ ( I ↾ (𝑠
∖ {∅})) ∈ V) |
47 | 45, 46 | ax-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
↾ (𝑠 ∖
{∅})) = (𝑠 ∖
{∅}) |
51 | 49, 50 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran
𝑓 = (𝑠 ∖ {∅})) |
52 | 51 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) →
(∅ ∈ ran 𝑓
↔ ∅ ∈ (𝑠
∖ {∅}))) |
53 | 52 | notbid 307 |
. . . . . . . . . 10
⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) →
(¬ ∅ ∈ ran 𝑓
↔ ¬ ∅ ∈ (𝑠 ∖ {∅}))) |
54 | 7, 53 | syl5bb 271 |
. . . . . . . . 9
⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) →
(∅ ∉ ran 𝑓
↔ ¬ ∅ ∈ (𝑠 ∖ {∅}))) |
55 | 48, 54 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) →
((Fun 𝑓 ∧ ∅
∉ ran 𝑓) ↔ (Fun
( I ↾ (𝑠 ∖
{∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})))) |
56 | | dmeq 5246 |
. . . . . . . . . . . 12
⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom
𝑓 = dom ( I ↾ (𝑠 ∖
{∅}))) |
57 | | dmresi 5376 |
. . . . . . . . . . . 12
⊢ dom ( I
↾ (𝑠 ∖
{∅})) = (𝑠 ∖
{∅}) |
58 | 56, 57 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom
𝑓 = (𝑠 ∖ {∅})) |
59 | 58 | ixpeq1d 7806 |
. . . . . . . . . 10
⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) →
X𝑥
∈ dom 𝑓(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})(𝑓‘𝑥)) |
60 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) →
(𝑓‘𝑥) = (( I ↾ (𝑠 ∖ {∅}))‘𝑥)) |
61 | | fvresi 6344 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑠 ∖ {∅}) → (( I ↾
(𝑠 ∖
{∅}))‘𝑥) =
𝑥) |
62 | 60, 61 | sylan9eq 2664 |
. . . . . . . . . . 11
⊢ ((𝑓 = ( I ↾ (𝑠 ∖ {∅})) ∧ 𝑥 ∈ (𝑠 ∖ {∅})) → (𝑓‘𝑥) = 𝑥) |
63 | 62 | ixpeq2dva 7809 |
. . . . . . . . . 10
⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) →
X𝑥
∈ (𝑠 ∖
{∅})(𝑓‘𝑥) = X𝑥 ∈
(𝑠 ∖ {∅})𝑥) |
64 | 59, 63 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) →
X𝑥
∈ dom 𝑓(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥) |
65 | 64 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) →
(X𝑥
∈ dom 𝑓(𝑓‘𝑥) ≠ ∅ ↔ X𝑥 ∈
(𝑠 ∖ {∅})𝑥 ≠ ∅)) |
66 | 55, 65 | imbi12d 333 |
. . . . . . 7
⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) →
(((Fun 𝑓 ∧ ∅
∉ ran 𝑓) → X𝑥 ∈
dom 𝑓(𝑓‘𝑥) ≠ ∅) ↔ ((Fun ( I ↾
(𝑠 ∖ {∅}))
∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈
(𝑠 ∖ {∅})𝑥 ≠
∅))) |
67 | 47, 66 | spcv 3272 |
. . . . . 6
⊢
(∀𝑓((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) → X𝑥 ∈
dom 𝑓(𝑓‘𝑥) ≠ ∅) → ((Fun ( I ↾
(𝑠 ∖ {∅}))
∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈
(𝑠 ∖ {∅})𝑥 ≠ ∅)) |
68 | 41, 42, 67 | mp2ani 710 |
. . . . 5
⊢
(∀𝑓((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) → X𝑥 ∈
dom 𝑓(𝑓‘𝑥) ≠ ∅) → X𝑥 ∈
(𝑠 ∖ {∅})𝑥 ≠ ∅) |
69 | | n0 3890 |
. . . . . 6
⊢ (X𝑥 ∈
(𝑠 ∖ {∅})𝑥 ≠ ∅ ↔
∃𝑔 𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥) |
70 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑔 ∈ V |
71 | 70 | elixp 7801 |
. . . . . . . 8
⊢ (𝑔 ∈ X𝑥 ∈
(𝑠 ∖ {∅})𝑥 ↔ (𝑔 Fn (𝑠 ∖ {∅}) ∧ ∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥)) |
72 | | eldifsn 4260 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑠 ∖ {∅}) ↔ (𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅)) |
73 | 72 | imbi1i 338 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔‘𝑥) ∈ 𝑥) ↔ ((𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅) → (𝑔‘𝑥) ∈ 𝑥)) |
74 | | impexp 461 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅) → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ∈ 𝑠 → (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))) |
75 | 73, 74 | bitri 263 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ∈ 𝑠 → (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))) |
76 | 75 | ralbii2 2961 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 ↔ ∀𝑥 ∈ 𝑠 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) |
77 | | neeq1 2844 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑡 → (𝑥 ≠ ∅ ↔ 𝑡 ≠ ∅)) |
78 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡)) |
79 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑡 → 𝑥 = 𝑡) |
80 | 78, 79 | eleq12d 2682 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑡 → ((𝑔‘𝑥) ∈ 𝑥 ↔ (𝑔‘𝑡) ∈ 𝑡)) |
81 | 77, 80 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑡 → ((𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))) |
82 | 81 | cbvralv 3147 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝑠 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) |
83 | 76, 82 | bitri 263 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
(𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 ↔ ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) |
84 | 83 | biimpi 205 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 → ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) |
85 | 84 | adantl 481 |
. . . . . . . 8
⊢ ((𝑔 Fn (𝑠 ∖ {∅}) ∧ ∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥) → ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) |
86 | 71, 85 | sylbi 206 |
. . . . . . 7
⊢ (𝑔 ∈ X𝑥 ∈
(𝑠 ∖ {∅})𝑥 → ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) |
87 | 86 | eximi 1752 |
. . . . . 6
⊢
(∃𝑔 𝑔 ∈ X𝑥 ∈
(𝑠 ∖ {∅})𝑥 → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) |
88 | 69, 87 | sylbi 206 |
. . . . 5
⊢ (X𝑥 ∈
(𝑠 ∖ {∅})𝑥 ≠ ∅ →
∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) |
89 | 68, 88 | syl 17 |
. . . 4
⊢
(∀𝑓((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) → X𝑥 ∈
dom 𝑓(𝑓‘𝑥) ≠ ∅) → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) |
90 | 89 | alrimiv 1842 |
. . 3
⊢
(∀𝑓((Fun
𝑓 ∧ ∅ ∉ ran
𝑓) → X𝑥 ∈
dom 𝑓(𝑓‘𝑥) ≠ ∅) → ∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) |
91 | 38, 90 | impbii 198 |
. 2
⊢
(∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅)) |
92 | 1, 91 | bitri 263 |
1
⊢
(CHOICE ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅)) |