Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. . . 4
⊢ 𝑥 ∈ V |
2 | | acacni 8845 |
. . . 4
⊢
((CHOICE ∧ 𝑥 ∈ V) → AC 𝑥 = V) |
3 | 1, 2 | mpan2 703 |
. . 3
⊢
(CHOICE → AC 𝑥 = V) |
4 | 3 | alrimiv 1842 |
. 2
⊢
(CHOICE → ∀𝑥AC 𝑥 = V) |
5 | | vex 3176 |
. . . . . . 7
⊢ 𝑦 ∈ V |
6 | | difexg 4735 |
. . . . . . 7
⊢ (𝑦 ∈ V → (𝑦 ∖ {∅}) ∈
V) |
7 | 5, 6 | ax-mp 5 |
. . . . . 6
⊢ (𝑦 ∖ {∅}) ∈
V |
8 | | acneq 8749 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∖ {∅}) → AC 𝑥 = AC (𝑦 ∖ {∅})) |
9 | 8 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∖ {∅}) → (AC 𝑥 = V ↔ AC (𝑦 ∖ {∅}) =
V)) |
10 | 7, 9 | spcv 3272 |
. . . . 5
⊢
(∀𝑥AC
𝑥 = V → AC
(𝑦 ∖ {∅}) =
V) |
11 | | vuniex 6852 |
. . . . . . 7
⊢ ∪ 𝑦
∈ V |
12 | | id 22 |
. . . . . . 7
⊢
(AC (𝑦
∖ {∅}) = V → AC (𝑦 ∖ {∅}) = V) |
13 | 11, 12 | syl5eleqr 2695 |
. . . . . 6
⊢
(AC (𝑦
∖ {∅}) = V → ∪ 𝑦 ∈ AC (𝑦 ∖ {∅})) |
14 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → 𝑧 ∈ 𝑦) |
15 | | elssuni 4403 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑦 → 𝑧 ⊆ ∪ 𝑦) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → 𝑧 ⊆ ∪ 𝑦) |
17 | | eldifsni 4261 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → 𝑧 ≠ ∅) |
18 | 16, 17 | jca 553 |
. . . . . . 7
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → (𝑧 ⊆ ∪ 𝑦
∧ 𝑧 ≠
∅)) |
19 | 18 | rgen 2906 |
. . . . . 6
⊢
∀𝑧 ∈
(𝑦 ∖ {∅})(𝑧 ⊆ ∪ 𝑦
∧ 𝑧 ≠
∅) |
20 | | acni2 8752 |
. . . . . 6
⊢ ((∪ 𝑦
∈ AC (𝑦 ∖
{∅}) ∧ ∀𝑧
∈ (𝑦 ∖
{∅})(𝑧 ⊆ ∪ 𝑦
∧ 𝑧 ≠ ∅))
→ ∃𝑔(𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧)) |
21 | 13, 19, 20 | sylancl 693 |
. . . . 5
⊢
(AC (𝑦
∖ {∅}) = V → ∃𝑔(𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧)) |
22 | 5 | mptex 6390 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) ∈ V |
23 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ (𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) |
24 | | eldifsn 4260 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅)) |
25 | 24 | imbi1i 338 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (𝑦 ∖ {∅}) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)) |
26 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (𝑔‘𝑥) = (𝑔‘𝑧)) |
27 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) |
28 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝑔‘𝑧) ∈ V |
29 | 26, 27, 28 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝑦 → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) = (𝑔‘𝑧)) |
30 | 14, 29 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) = (𝑔‘𝑧)) |
31 | 30 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → (((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧 ↔ (𝑔‘𝑧) ∈ 𝑧)) |
32 | 31 | pm5.74i 259 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (𝑦 ∖ {∅}) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧) ↔ (𝑧 ∈ (𝑦 ∖ {∅}) → (𝑔‘𝑧) ∈ 𝑧)) |
33 | | impexp 461 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧) ↔ (𝑧 ∈ 𝑦 → (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))) |
34 | 25, 32, 33 | 3bitr3i 289 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (𝑦 ∖ {∅}) → (𝑔‘𝑧) ∈ 𝑧) ↔ (𝑧 ∈ 𝑦 → (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))) |
35 | 34 | ralbii2 2961 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧 ↔ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)) |
36 | 23, 35 | sylib 207 |
. . . . . . . 8
⊢ ((𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)) |
37 | | fvrn0 6126 |
. . . . . . . . . . 11
⊢ (𝑔‘𝑥) ∈ (ran 𝑔 ∪ {∅}) |
38 | 37 | rgenw 2908 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
𝑦 (𝑔‘𝑥) ∈ (ran 𝑔 ∪ {∅}) |
39 | 27 | fmpt 6289 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑦 (𝑔‘𝑥) ∈ (ran 𝑔 ∪ {∅}) ↔ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)):𝑦⟶(ran 𝑔 ∪ {∅})) |
40 | 38, 39 | mpbi 219 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)):𝑦⟶(ran 𝑔 ∪ {∅}) |
41 | | ffn 5958 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)):𝑦⟶(ran 𝑔 ∪ {∅}) → (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦 |
43 | 36, 42 | jctil 558 |
. . . . . . 7
⊢ ((𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))) |
44 | | fneq1 5893 |
. . . . . . . . 9
⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → (𝑓 Fn 𝑦 ↔ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦)) |
45 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → (𝑓‘𝑧) = ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧)) |
46 | 45 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → ((𝑓‘𝑧) ∈ 𝑧 ↔ ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)) |
47 | 46 | imbi2d 329 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))) |
48 | 47 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → (∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))) |
49 | 44, 48 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → ((𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ↔ ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)))) |
50 | 49 | spcegv 3267 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) ∈ V → (((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))) |
51 | 22, 43, 50 | mpsyl 66 |
. . . . . 6
⊢ ((𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
52 | 51 | exlimiv 1845 |
. . . . 5
⊢
(∃𝑔(𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
53 | 10, 21, 52 | 3syl 18 |
. . . 4
⊢
(∀𝑥AC
𝑥 = V → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
54 | 53 | alrimiv 1842 |
. . 3
⊢
(∀𝑥AC
𝑥 = V → ∀𝑦∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
55 | | dfac4 8828 |
. . 3
⊢
(CHOICE ↔ ∀𝑦∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
56 | 54, 55 | sylibr 223 |
. 2
⊢
(∀𝑥AC
𝑥 = V →
CHOICE) |
57 | 4, 56 | impbii 198 |
1
⊢
(CHOICE ↔ ∀𝑥AC 𝑥 = V) |