Step |
Hyp |
Ref |
Expression |
1 |
|
riotauni |
⊢ ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → ( ℩ 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) = ∪ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) |
2 |
|
riotacl |
⊢ ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → ( ℩ 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ∈ 𝑧 ) |
3 |
1 2
|
eqeltrrd |
⊢ ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → ∪ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ∈ 𝑧 ) |
4 |
|
elequ2 |
⊢ ( 𝑢 = 𝑧 → ( 𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑧 ) ) |
5 |
|
elequ1 |
⊢ ( 𝑢 = 𝑧 → ( 𝑢 ∈ 𝑣 ↔ 𝑧 ∈ 𝑣 ) ) |
6 |
5
|
anbi1d |
⊢ ( 𝑢 = 𝑧 → ( ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) |
7 |
6
|
rexbidv |
⊢ ( 𝑢 = 𝑧 → ( ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) |
8 |
4 7
|
anbi12d |
⊢ ( 𝑢 = 𝑧 → ( ( 𝑤 ∈ 𝑢 ∧ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ↔ ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) ) |
9 |
8
|
rabbidva2 |
⊢ ( 𝑢 = 𝑧 → { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } = { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) |
10 |
9
|
unieqd |
⊢ ( 𝑢 = 𝑧 → ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } = ∪ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) |
11 |
|
eqid |
⊢ ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) = ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) |
12 |
|
vex |
⊢ 𝑧 ∈ V |
13 |
12
|
rabex |
⊢ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ∈ V |
14 |
13
|
uniex |
⊢ ∪ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ∈ V |
15 |
10 11 14
|
fvmpt |
⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) = ∪ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) |
16 |
15
|
eleq1d |
⊢ ( 𝑧 ∈ 𝑥 → ( ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ↔ ∪ { 𝑤 ∈ 𝑧 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ∈ 𝑧 ) ) |
17 |
3 16
|
syl5ibr |
⊢ ( 𝑧 ∈ 𝑥 → ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) ) |
18 |
17
|
imim2d |
⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ( 𝑧 ≠ ∅ → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
19 |
18
|
ralimia |
⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) ) |
20 |
|
ssrab2 |
⊢ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ⊆ 𝑢 |
21 |
|
elssuni |
⊢ ( 𝑢 ∈ 𝑥 → 𝑢 ⊆ ∪ 𝑥 ) |
22 |
20 21
|
sstrid |
⊢ ( 𝑢 ∈ 𝑥 → { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ⊆ ∪ 𝑥 ) |
23 |
22
|
unissd |
⊢ ( 𝑢 ∈ 𝑥 → ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ⊆ ∪ ∪ 𝑥 ) |
24 |
|
vex |
⊢ 𝑥 ∈ V |
25 |
24
|
uniex |
⊢ ∪ 𝑥 ∈ V |
26 |
25
|
uniex |
⊢ ∪ ∪ 𝑥 ∈ V |
27 |
26
|
elpw2 |
⊢ ( ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ∈ 𝒫 ∪ ∪ 𝑥 ↔ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ⊆ ∪ ∪ 𝑥 ) |
28 |
23 27
|
sylibr |
⊢ ( 𝑢 ∈ 𝑥 → ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ∈ 𝒫 ∪ ∪ 𝑥 ) |
29 |
11 28
|
fmpti |
⊢ ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) : 𝑥 ⟶ 𝒫 ∪ ∪ 𝑥 |
30 |
26
|
pwex |
⊢ 𝒫 ∪ ∪ 𝑥 ∈ V |
31 |
|
fex2 |
⊢ ( ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) : 𝑥 ⟶ 𝒫 ∪ ∪ 𝑥 ∧ 𝑥 ∈ V ∧ 𝒫 ∪ ∪ 𝑥 ∈ V ) → ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ∈ V ) |
32 |
29 24 30 31
|
mp3an |
⊢ ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ∈ V |
33 |
|
fveq1 |
⊢ ( 𝑓 = ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) → ( 𝑓 ‘ 𝑧 ) = ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ) |
34 |
33
|
eleq1d |
⊢ ( 𝑓 = ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) ) |
35 |
34
|
imbi2d |
⊢ ( 𝑓 = ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) → ( ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
36 |
35
|
ralbidv |
⊢ ( 𝑓 = ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
37 |
32 36
|
spcev |
⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) |
38 |
19 37
|
syl |
⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) |
39 |
38
|
exlimiv |
⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) |
40 |
39
|
alimi |
⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) |
41 |
|
dfac3 |
⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) |
42 |
40 41
|
sylibr |
⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → CHOICE ) |