Step |
Hyp |
Ref |
Expression |
0 |
|
cA |
⊢ 𝐴 |
1 |
0
|
wacn |
⊢ AC 𝐴 |
2 |
|
vx |
⊢ 𝑥 |
3 |
|
cvv |
⊢ V |
4 |
0 3
|
wcel |
⊢ 𝐴 ∈ V |
5 |
|
vf |
⊢ 𝑓 |
6 |
2
|
cv |
⊢ 𝑥 |
7 |
6
|
cpw |
⊢ 𝒫 𝑥 |
8 |
|
c0 |
⊢ ∅ |
9 |
8
|
csn |
⊢ { ∅ } |
10 |
7 9
|
cdif |
⊢ ( 𝒫 𝑥 ∖ { ∅ } ) |
11 |
|
cmap |
⊢ ↑m |
12 |
10 0 11
|
co |
⊢ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) |
13 |
|
vg |
⊢ 𝑔 |
14 |
|
vy |
⊢ 𝑦 |
15 |
13
|
cv |
⊢ 𝑔 |
16 |
14
|
cv |
⊢ 𝑦 |
17 |
16 15
|
cfv |
⊢ ( 𝑔 ‘ 𝑦 ) |
18 |
5
|
cv |
⊢ 𝑓 |
19 |
16 18
|
cfv |
⊢ ( 𝑓 ‘ 𝑦 ) |
20 |
17 19
|
wcel |
⊢ ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) |
21 |
20 14 0
|
wral |
⊢ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) |
22 |
21 13
|
wex |
⊢ ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) |
23 |
22 5 12
|
wral |
⊢ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) |
24 |
4 23
|
wa |
⊢ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) |
25 |
24 2
|
cab |
⊢ { 𝑥 ∣ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) } |
26 |
1 25
|
wceq |
⊢ AC 𝐴 = { 𝑥 ∣ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) } |