Step |
Hyp |
Ref |
Expression |
1 |
|
biidd |
⊢ ( 𝑤 = 𝑡 → ( ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) ) |
2 |
1
|
cbvralvw |
⊢ ( ∀ 𝑤 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑡 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) |
3 |
|
elequ1 |
⊢ ( 𝑣 = 𝑧 → ( 𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢 ) ) |
4 |
3
|
anbi2d |
⊢ ( 𝑣 = 𝑧 → ( ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ) |
5 |
4
|
rexbidv |
⊢ ( 𝑣 = 𝑧 → ( ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ) |
6 |
5
|
cbvreuvw |
⊢ ( ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) |
7 |
6
|
ralbii |
⊢ ( ∀ 𝑡 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑡 ∈ ℎ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) |
8 |
2 7
|
bitri |
⊢ ( ∀ 𝑤 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑡 ∈ ℎ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) |
9 |
8
|
ralbii |
⊢ ( ∀ ℎ ∈ 𝑥 ∀ 𝑤 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ ℎ ∈ 𝑥 ∀ 𝑡 ∈ ℎ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) |
10 |
|
elequ1 |
⊢ ( 𝑧 = ℎ → ( 𝑧 ∈ 𝑢 ↔ ℎ ∈ 𝑢 ) ) |
11 |
10
|
anbi1d |
⊢ ( 𝑧 = ℎ → ( ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) ) |
12 |
11
|
rexbidv |
⊢ ( 𝑧 = ℎ → ( ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) ) |
13 |
12
|
reueqd |
⊢ ( 𝑧 = ℎ → ( ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) ) |
14 |
13
|
raleqbi1dv |
⊢ ( 𝑧 = ℎ → ( ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑤 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) ) |
15 |
14
|
cbvralvw |
⊢ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ ℎ ∈ 𝑥 ∀ 𝑤 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) |
16 |
|
elequ1 |
⊢ ( 𝑤 = ℎ → ( 𝑤 ∈ 𝑢 ↔ ℎ ∈ 𝑢 ) ) |
17 |
16
|
anbi1d |
⊢ ( 𝑤 = ℎ → ( ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ) |
18 |
17
|
rexbidv |
⊢ ( 𝑤 = ℎ → ( ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ) |
19 |
18
|
reueqd |
⊢ ( 𝑤 = ℎ → ( ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ) |
20 |
19
|
raleqbi1dv |
⊢ ( 𝑤 = ℎ → ( ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∀ 𝑡 ∈ ℎ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ) |
21 |
20
|
cbvralvw |
⊢ ( ∀ 𝑤 ∈ 𝑥 ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∀ ℎ ∈ 𝑥 ∀ 𝑡 ∈ ℎ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) |
22 |
9 15 21
|
3bitr4i |
⊢ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑤 ∈ 𝑥 ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) |
23 |
22
|
exbii |
⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃ 𝑦 ∀ 𝑤 ∈ 𝑥 ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) |
24 |
|
19.21v |
⊢ ( ∀ 𝑧 ( 𝑤 ∈ 𝑥 → ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) ↔ ( 𝑤 ∈ 𝑥 → ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) ) |
25 |
|
impexp |
⊢ ( ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑤 → ( 𝑤 ∈ 𝑥 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) ) |
26 |
|
bi2.04 |
⊢ ( ( 𝑧 ∈ 𝑤 → ( 𝑤 ∈ 𝑥 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) ↔ ( 𝑤 ∈ 𝑥 → ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) ) |
27 |
25 26
|
bitri |
⊢ ( ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ( 𝑤 ∈ 𝑥 → ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) ) |
28 |
27
|
albii |
⊢ ( ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ∀ 𝑧 ( 𝑤 ∈ 𝑥 → ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) ) |
29 |
|
eu6 |
⊢ ( ∃! 𝑧 ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ∃ 𝑥 ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ 𝑧 = 𝑥 ) ) |
30 |
|
df-reu |
⊢ ( ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃! 𝑧 ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ) |
31 |
|
19.42v |
⊢ ( ∃ 𝑥 ( 𝑧 ∈ 𝑤 ∧ ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) ↔ ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) ) |
32 |
|
an42 |
⊢ ( ( ( 𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦 ) ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ↔ ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ) |
33 |
|
anass |
⊢ ( ( ( 𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦 ) ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑤 ∧ ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) ) |
34 |
32 33
|
bitr3i |
⊢ ( ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝑤 ∧ ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) ) |
35 |
34
|
exbii |
⊢ ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ ∃ 𝑥 ( 𝑧 ∈ 𝑤 ∧ ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) ) |
36 |
|
df-rex |
⊢ ( ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ) |
37 |
|
elequ1 |
⊢ ( 𝑢 = 𝑥 → ( 𝑢 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) ) |
38 |
|
elequ2 |
⊢ ( 𝑢 = 𝑥 → ( 𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑥 ) ) |
39 |
|
elequ2 |
⊢ ( 𝑢 = 𝑥 → ( 𝑧 ∈ 𝑢 ↔ 𝑧 ∈ 𝑥 ) ) |
40 |
38 39
|
anbi12d |
⊢ ( 𝑢 = 𝑥 → ( ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) |
41 |
37 40
|
anbi12d |
⊢ ( 𝑢 = 𝑥 → ( ( 𝑢 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) ) |
42 |
41
|
cbvexvw |
⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) |
43 |
36 42
|
bitri |
⊢ ( ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) |
44 |
43
|
anbi2i |
⊢ ( ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) ) |
45 |
31 35 44
|
3bitr4i |
⊢ ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ) |
46 |
45
|
bibi1i |
⊢ ( ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ↔ ( ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ 𝑧 = 𝑥 ) ) |
47 |
46
|
albii |
⊢ ( ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ↔ ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ 𝑧 = 𝑥 ) ) |
48 |
47
|
exbii |
⊢ ( ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ↔ ∃ 𝑥 ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ 𝑧 = 𝑥 ) ) |
49 |
29 30 48
|
3bitr4i |
⊢ ( ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) |
50 |
49
|
imbi2i |
⊢ ( ( 𝑡 ∈ 𝑤 → ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ( 𝑡 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) |
51 |
50
|
albii |
⊢ ( ∀ 𝑡 ( 𝑡 ∈ 𝑤 → ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) |
52 |
|
df-ral |
⊢ ( ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑤 → ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ) |
53 |
|
nfv |
⊢ Ⅎ 𝑡 ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) |
54 |
|
nfv |
⊢ Ⅎ 𝑧 𝑡 ∈ 𝑤 |
55 |
|
nfa1 |
⊢ Ⅎ 𝑧 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) |
56 |
55
|
nfex |
⊢ Ⅎ 𝑧 ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) |
57 |
54 56
|
nfim |
⊢ Ⅎ 𝑧 ( 𝑡 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) |
58 |
|
elequ1 |
⊢ ( 𝑧 = 𝑡 → ( 𝑧 ∈ 𝑤 ↔ 𝑡 ∈ 𝑤 ) ) |
59 |
58
|
imbi1d |
⊢ ( 𝑧 = 𝑡 → ( ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ( 𝑡 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) ) |
60 |
53 57 59
|
cbvalv1 |
⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) |
61 |
51 52 60
|
3bitr4i |
⊢ ( ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) |
62 |
61
|
imbi2i |
⊢ ( ( 𝑤 ∈ 𝑥 → ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ( 𝑤 ∈ 𝑥 → ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) ) |
63 |
24 28 62
|
3bitr4i |
⊢ ( ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ( 𝑤 ∈ 𝑥 → ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ) |
64 |
63
|
albii |
⊢ ( ∀ 𝑤 ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ) |
65 |
|
alcom |
⊢ ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ∀ 𝑤 ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) |
66 |
|
df-ral |
⊢ ( ∀ 𝑤 ∈ 𝑥 ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ) |
67 |
64 65 66
|
3bitr4ri |
⊢ ( ∀ 𝑤 ∈ 𝑥 ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) |
68 |
67
|
exbii |
⊢ ( ∃ 𝑦 ∀ 𝑤 ∈ 𝑥 ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃ 𝑦 ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) |
69 |
23 68
|
bitri |
⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃ 𝑦 ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) |