Step |
Hyp |
Ref |
Expression |
1 |
|
axgroth4 |
⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) |
2 |
|
3anass |
⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ) ) |
3 |
|
dfss2 |
⊢ ( 𝑤 ⊆ 𝑧 ↔ ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) ) |
4 |
|
elin |
⊢ ( 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ↔ ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) |
5 |
3 4
|
imbi12i |
⊢ ( ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) |
6 |
5
|
albii |
⊢ ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) |
7 |
6
|
rexbii |
⊢ ( ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) |
8 |
|
df-rex |
⊢ ( ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) |
9 |
7 8
|
bitri |
⊢ ( ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) |
10 |
9
|
ralbii |
⊢ ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) |
11 |
|
df-ral |
⊢ ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ) |
12 |
10 11
|
bitri |
⊢ ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ) |
13 |
|
dfss2 |
⊢ ( 𝑧 ⊆ 𝑦 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) |
14 |
|
vex |
⊢ 𝑦 ∈ V |
15 |
14
|
difexi |
⊢ ( 𝑦 ∖ 𝑧 ) ∈ V |
16 |
|
vex |
⊢ 𝑧 ∈ V |
17 |
|
disjdifr |
⊢ ( ( 𝑦 ∖ 𝑧 ) ∩ 𝑧 ) = ∅ |
18 |
15 16 17
|
brdom6disj |
⊢ ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ↔ ∃ 𝑤 ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ) |
19 |
18
|
orbi1i |
⊢ ( ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ↔ ( ∃ 𝑤 ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) |
20 |
|
19.44v |
⊢ ( ∃ 𝑤 ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ↔ ( ∃ 𝑤 ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) |
21 |
19 20
|
bitr4i |
⊢ ( ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑤 ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) |
22 |
13 21
|
imbi12i |
⊢ ( ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ∃ 𝑤 ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) ) |
23 |
|
19.35 |
⊢ ( ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ∃ 𝑤 ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) ) |
24 |
22 23
|
bitr4i |
⊢ ( ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) ) |
25 |
|
grothprimlem |
⊢ ( { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) ) |
26 |
25
|
mobii |
⊢ ( ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∃* 𝑢 ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) ) |
27 |
|
df-mo |
⊢ ( ∃* 𝑢 ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) ↔ ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) |
28 |
26 27
|
bitri |
⊢ ( ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) |
29 |
28
|
ralbii |
⊢ ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∀ 𝑣 ∈ 𝑧 ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) |
30 |
|
df-ral |
⊢ ( ∀ 𝑣 ∈ 𝑧 ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ↔ ∀ 𝑣 ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ) |
31 |
29 30
|
bitri |
⊢ ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ↔ ∀ 𝑣 ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ) |
32 |
|
df-ral |
⊢ ( ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∀ 𝑣 ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) → ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ) |
33 |
|
eldif |
⊢ ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ↔ ( 𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧 ) ) |
34 |
|
grothprimlem |
⊢ ( { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) |
35 |
34
|
rexbii |
⊢ ( ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∃ 𝑢 ∈ 𝑧 ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) |
36 |
|
df-rex |
⊢ ( ∃ 𝑢 ∈ 𝑧 ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) |
37 |
35 36
|
bitri |
⊢ ( ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) |
38 |
33 37
|
imbi12i |
⊢ ( ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) → ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ( ( 𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧 ) → ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) |
39 |
|
pm5.6 |
⊢ ( ( ( 𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧 ) → ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ↔ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) |
40 |
38 39
|
bitri |
⊢ ( ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) → ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) |
41 |
40
|
albii |
⊢ ( ∀ 𝑣 ( 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) → ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ∀ 𝑣 ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) |
42 |
32 41
|
bitri |
⊢ ( ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∀ 𝑣 ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) |
43 |
31 42
|
anbi12i |
⊢ ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ( ∀ 𝑣 ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ) |
44 |
|
19.26 |
⊢ ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ↔ ( ∀ 𝑣 ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ∀ 𝑣 ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ) |
45 |
43 44
|
bitr4i |
⊢ ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ↔ ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ) |
46 |
45
|
orbi1i |
⊢ ( ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) |
47 |
46
|
imbi2i |
⊢ ( ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) |
48 |
47
|
exbii |
⊢ ( ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ( ∀ 𝑣 ∈ 𝑧 ∃* 𝑢 { 𝑣 , 𝑢 } ∈ 𝑤 ∧ ∀ 𝑣 ∈ ( 𝑦 ∖ 𝑧 ) ∃ 𝑢 ∈ 𝑧 { 𝑢 , 𝑣 } ∈ 𝑤 ) ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) |
49 |
24 48
|
bitri |
⊢ ( ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) |
50 |
49
|
albii |
⊢ ( ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ∀ 𝑧 ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) |
51 |
12 50
|
anbi12i |
⊢ ( ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∀ 𝑧 ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ) |
52 |
|
19.26 |
⊢ ( ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∀ 𝑧 ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ) |
53 |
51 52
|
bitr4i |
⊢ ( ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ) |
54 |
53
|
anbi2i |
⊢ ( ( 𝑥 ∈ 𝑦 ∧ ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ) ) |
55 |
2 54
|
bitri |
⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ) ) |
56 |
55
|
exbii |
⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ) ) |
57 |
1 56
|
mpbi |
⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( ( 𝑧 ∈ 𝑦 → ∃ 𝑣 ( 𝑣 ∈ 𝑦 ∧ ∀ 𝑤 ( ∀ 𝑢 ( 𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ∧ ∃ 𝑤 ( ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) → ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑧 → ∃ 𝑡 ∀ 𝑢 ( ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑣 ∨ ℎ = 𝑢 ) ) ) → 𝑢 = 𝑡 ) ) ∧ ( 𝑣 ∈ 𝑦 → ( 𝑣 ∈ 𝑧 ∨ ∃ 𝑢 ( 𝑢 ∈ 𝑧 ∧ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) ) ) ) ) ∨ 𝑧 ∈ 𝑦 ) ) ) ) |