Step |
Hyp |
Ref |
Expression |
1 |
|
df-ral |
⊢ ( ∀ 𝑡 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑧 → ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) ) |
2 |
|
19.23v |
⊢ ( ∀ 𝑡 ( 𝑡 ∈ 𝑧 → ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) ↔ ( ∃ 𝑡 𝑡 ∈ 𝑧 → ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) ) |
3 |
1 2
|
bitri |
⊢ ( ∀ 𝑡 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ( ∃ 𝑡 𝑡 ∈ 𝑧 → ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) ) |
4 |
|
biidd |
⊢ ( 𝑤 = 𝑡 → ( ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) ) |
5 |
4
|
cbvralvw |
⊢ ( ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑡 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) |
6 |
|
n0 |
⊢ ( 𝑧 ≠ ∅ ↔ ∃ 𝑡 𝑡 ∈ 𝑧 ) |
7 |
|
elequ2 |
⊢ ( 𝑣 = 𝑢 → ( 𝑧 ∈ 𝑣 ↔ 𝑧 ∈ 𝑢 ) ) |
8 |
|
elequ2 |
⊢ ( 𝑣 = 𝑢 → ( 𝑤 ∈ 𝑣 ↔ 𝑤 ∈ 𝑢 ) ) |
9 |
7 8
|
anbi12d |
⊢ ( 𝑣 = 𝑢 → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ( 𝑧 ∈ 𝑢 ∧ 𝑤 ∈ 𝑢 ) ) ) |
10 |
9
|
cbvrexvw |
⊢ ( ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑤 ∈ 𝑢 ) ) |
11 |
10
|
reubii |
⊢ ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ∃! 𝑤 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑤 ∈ 𝑢 ) ) |
12 |
|
elequ1 |
⊢ ( 𝑤 = 𝑣 → ( 𝑤 ∈ 𝑢 ↔ 𝑣 ∈ 𝑢 ) ) |
13 |
12
|
anbi2d |
⊢ ( 𝑤 = 𝑣 → ( ( 𝑧 ∈ 𝑢 ∧ 𝑤 ∈ 𝑢 ) ↔ ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) ) |
14 |
13
|
rexbidv |
⊢ ( 𝑤 = 𝑣 → ( ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑤 ∈ 𝑢 ) ↔ ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) ) |
15 |
14
|
cbvreuvw |
⊢ ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑤 ∈ 𝑢 ) ↔ ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) |
16 |
11 15
|
bitri |
⊢ ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) |
17 |
6 16
|
imbi12i |
⊢ ( ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ↔ ( ∃ 𝑡 𝑡 ∈ 𝑧 → ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) ) |
18 |
3 5 17
|
3bitr4i |
⊢ ( ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) |
19 |
18
|
ralbii |
⊢ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) |
20 |
19
|
exbii |
⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) |