Step |
Hyp |
Ref |
Expression |
1 |
|
dfac3 |
⊢ ( CHOICE ↔ ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) |
2 |
|
vex |
⊢ 𝑥 ∈ V |
3 |
|
vpwex |
⊢ 𝒫 𝑥 ∈ V |
4 |
|
raleq |
⊢ ( 𝑦 = 𝒫 𝑥 → ( ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝒫 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
5 |
4
|
exbidv |
⊢ ( 𝑦 = 𝒫 𝑥 → ( ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∃ 𝑓 ∀ 𝑧 ∈ 𝒫 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
6 |
3 5
|
spcv |
⊢ ( ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝒫 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) |
7 |
|
dfac8a |
⊢ ( 𝑥 ∈ V → ( ∃ 𝑓 ∀ 𝑧 ∈ 𝒫 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → 𝑥 ∈ dom card ) ) |
8 |
2 6 7
|
mpsyl |
⊢ ( ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → 𝑥 ∈ dom card ) |
9 |
|
dfac8b |
⊢ ( 𝑥 ∈ dom card → ∃ 𝑟 𝑟 We 𝑥 ) |
10 |
8 9
|
syl |
⊢ ( ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑟 𝑟 We 𝑥 ) |
11 |
10
|
alrimiv |
⊢ ( ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 ) |
12 |
|
vex |
⊢ 𝑦 ∈ V |
13 |
|
vuniex |
⊢ ∪ 𝑦 ∈ V |
14 |
|
weeq2 |
⊢ ( 𝑥 = ∪ 𝑦 → ( 𝑟 We 𝑥 ↔ 𝑟 We ∪ 𝑦 ) ) |
15 |
14
|
exbidv |
⊢ ( 𝑥 = ∪ 𝑦 → ( ∃ 𝑟 𝑟 We 𝑥 ↔ ∃ 𝑟 𝑟 We ∪ 𝑦 ) ) |
16 |
13 15
|
spcv |
⊢ ( ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 → ∃ 𝑟 𝑟 We ∪ 𝑦 ) |
17 |
|
dfac8c |
⊢ ( 𝑦 ∈ V → ( ∃ 𝑟 𝑟 We ∪ 𝑦 → ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
18 |
12 16 17
|
mpsyl |
⊢ ( ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 → ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) |
19 |
18
|
alrimiv |
⊢ ( ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 → ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) |
20 |
11 19
|
impbii |
⊢ ( ∀ 𝑦 ∃ 𝑓 ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 ) |
21 |
1 20
|
bitri |
⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 ) |