Step | Hyp | Ref
| Expression |
1 | | vex 3354 |
. . . 4
⊢ 𝑥 ∈ V |
2 | | acacni 9164 |
. . . 4
⊢
((CHOICE ∧ 𝑥 ∈ V) → AC 𝑥 = V) |
3 | 1, 2 | mpan2 671 |
. . 3
⊢
(CHOICE → AC 𝑥 = V) |
4 | 3 | alrimiv 2007 |
. 2
⊢
(CHOICE → ∀𝑥AC 𝑥 = V) |
5 | | vex 3354 |
. . . . . . 7
⊢ 𝑦 ∈ V |
6 | | difexg 4942 |
. . . . . . 7
⊢ (𝑦 ∈ V → (𝑦 ∖ {∅}) ∈
V) |
7 | 5, 6 | ax-mp 5 |
. . . . . 6
⊢ (𝑦 ∖ {∅}) ∈
V |
8 | | acneq 9066 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∖ {∅}) → AC 𝑥 = AC (𝑦 ∖ {∅})) |
9 | 8 | eqeq1d 2773 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∖ {∅}) → (AC 𝑥 = V ↔ AC (𝑦 ∖ {∅}) =
V)) |
10 | 7, 9 | spcv 3450 |
. . . . 5
⊢
(∀𝑥AC
𝑥 = V → AC
(𝑦 ∖ {∅}) =
V) |
11 | | vuniex 7101 |
. . . . . . 7
⊢ ∪ 𝑦
∈ V |
12 | | id 22 |
. . . . . . 7
⊢
(AC (𝑦
∖ {∅}) = V → AC (𝑦 ∖ {∅}) = V) |
13 | 11, 12 | syl5eleqr 2857 |
. . . . . 6
⊢
(AC (𝑦
∖ {∅}) = V → ∪ 𝑦 ∈ AC (𝑦 ∖ {∅})) |
14 | | eldifi 3883 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → 𝑧 ∈ 𝑦) |
15 | | elssuni 4603 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑦 → 𝑧 ⊆ ∪ 𝑦) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → 𝑧 ⊆ ∪ 𝑦) |
17 | | eldifsni 4457 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → 𝑧 ≠ ∅) |
18 | 16, 17 | jca 501 |
. . . . . . 7
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → (𝑧 ⊆ ∪ 𝑦
∧ 𝑧 ≠
∅)) |
19 | 18 | rgen 3071 |
. . . . . 6
⊢
∀𝑧 ∈
(𝑦 ∖ {∅})(𝑧 ⊆ ∪ 𝑦
∧ 𝑧 ≠
∅) |
20 | | acni2 9069 |
. . . . . 6
⊢ ((∪ 𝑦
∈ AC (𝑦 ∖
{∅}) ∧ ∀𝑧
∈ (𝑦 ∖
{∅})(𝑧 ⊆ ∪ 𝑦
∧ 𝑧 ≠ ∅))
→ ∃𝑔(𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧)) |
21 | 13, 19, 20 | sylancl 574 |
. . . . 5
⊢
(AC (𝑦
∖ {∅}) = V → ∃𝑔(𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧)) |
22 | 5 | mptex 6630 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) ∈ V |
23 | | simpr 471 |
. . . . . . . . 9
⊢ ((𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ (𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) |
24 | | eldifsn 4453 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅)) |
25 | 24 | imbi1i 338 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (𝑦 ∖ {∅}) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)) |
26 | | fveq2 6332 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (𝑔‘𝑥) = (𝑔‘𝑧)) |
27 | | eqid 2771 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) |
28 | | fvex 6342 |
. . . . . . . . . . . . . . 15
⊢ (𝑔‘𝑧) ∈ V |
29 | 26, 27, 28 | fvmpt 6424 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝑦 → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) = (𝑔‘𝑧)) |
30 | 14, 29 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) = (𝑔‘𝑧)) |
31 | 30 | eleq1d 2835 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑦 ∖ {∅}) → (((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧 ↔ (𝑔‘𝑧) ∈ 𝑧)) |
32 | 31 | pm5.74i 260 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (𝑦 ∖ {∅}) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧) ↔ (𝑧 ∈ (𝑦 ∖ {∅}) → (𝑔‘𝑧) ∈ 𝑧)) |
33 | | impexp 437 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧) ↔ (𝑧 ∈ 𝑦 → (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))) |
34 | 25, 32, 33 | 3bitr3i 290 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (𝑦 ∖ {∅}) → (𝑔‘𝑧) ∈ 𝑧) ↔ (𝑧 ∈ 𝑦 → (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))) |
35 | 34 | ralbii2 3127 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧 ↔ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)) |
36 | 23, 35 | sylib 208 |
. . . . . . . 8
⊢ ((𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)) |
37 | | fvrn0 6357 |
. . . . . . . . . . 11
⊢ (𝑔‘𝑥) ∈ (ran 𝑔 ∪ {∅}) |
38 | 37 | rgenw 3073 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
𝑦 (𝑔‘𝑥) ∈ (ran 𝑔 ∪ {∅}) |
39 | 27 | fmpt 6523 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑦 (𝑔‘𝑥) ∈ (ran 𝑔 ∪ {∅}) ↔ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)):𝑦⟶(ran 𝑔 ∪ {∅})) |
40 | 38, 39 | mpbi 220 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)):𝑦⟶(ran 𝑔 ∪ {∅}) |
41 | | ffn 6185 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)):𝑦⟶(ran 𝑔 ∪ {∅}) → (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦 |
43 | 36, 42 | jctil 509 |
. . . . . . 7
⊢ ((𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))) |
44 | | fneq1 6119 |
. . . . . . . . 9
⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → (𝑓 Fn 𝑦 ↔ (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦)) |
45 | | fveq1 6331 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → (𝑓‘𝑧) = ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧)) |
46 | 45 | eleq1d 2835 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → ((𝑓‘𝑧) ∈ 𝑧 ↔ ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)) |
47 | 46 | imbi2d 329 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))) |
48 | 47 | ralbidv 3135 |
. . . . . . . . 9
⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → (∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧))) |
49 | 44, 48 | anbi12d 616 |
. . . . . . . 8
⊢ (𝑓 = (𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) → ((𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ↔ ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)))) |
50 | 49 | spcegv 3445 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) ∈ V → (((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥)) Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → ((𝑥 ∈ 𝑦 ↦ (𝑔‘𝑥))‘𝑧) ∈ 𝑧)) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))) |
51 | 22, 43, 50 | mpsyl 68 |
. . . . . 6
⊢ ((𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
52 | 51 | exlimiv 2010 |
. . . . 5
⊢
(∃𝑔(𝑔:(𝑦 ∖ {∅})⟶∪ 𝑦
∧ ∀𝑧 ∈
(𝑦 ∖ {∅})(𝑔‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
53 | 10, 21, 52 | 3syl 18 |
. . . 4
⊢
(∀𝑥AC
𝑥 = V → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
54 | 53 | alrimiv 2007 |
. . 3
⊢
(∀𝑥AC
𝑥 = V → ∀𝑦∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
55 | | dfac4 9145 |
. . 3
⊢
(CHOICE ↔ ∀𝑦∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
56 | 54, 55 | sylibr 224 |
. 2
⊢
(∀𝑥AC
𝑥 = V →
CHOICE) |
57 | 4, 56 | impbii 199 |
1
⊢
(CHOICE ↔ ∀𝑥AC 𝑥 = V) |