Step |
Hyp |
Ref |
Expression |
1 |
|
axtrkg.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
2 |
|
axtrkg.d |
⊢ − = ( dist ‘ 𝐺 ) |
3 |
|
axtrkg.i |
⊢ 𝐼 = ( Itv ‘ 𝐺 ) |
4 |
|
axtrkg.g |
⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) |
5 |
|
axtgcont.1 |
⊢ ( 𝜑 → 𝑆 ⊆ 𝑃 ) |
6 |
|
axtgcont.2 |
⊢ ( 𝜑 → 𝑇 ⊆ 𝑃 ) |
7 |
|
axtgcont.3 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) |
8 |
|
axtgcont.4 |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑇 ) → 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) ) |
9 |
8
|
3expb |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑇 ) ) → 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) ) |
10 |
9
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑇 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) ) |
11 |
|
simplr |
⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑥 = 𝑢 ) ∧ 𝑦 = 𝑣 ) → 𝑥 = 𝑢 ) |
12 |
|
simpll |
⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑥 = 𝑢 ) ∧ 𝑦 = 𝑣 ) → 𝑎 = 𝐴 ) |
13 |
|
simpr |
⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑥 = 𝑢 ) ∧ 𝑦 = 𝑣 ) → 𝑦 = 𝑣 ) |
14 |
12 13
|
oveq12d |
⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑥 = 𝑢 ) ∧ 𝑦 = 𝑣 ) → ( 𝑎 𝐼 𝑦 ) = ( 𝐴 𝐼 𝑣 ) ) |
15 |
11 14
|
eleq12d |
⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑥 = 𝑢 ) ∧ 𝑦 = 𝑣 ) → ( 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) ) ) |
16 |
15
|
cbvraldva |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑥 = 𝑢 ) → ( ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∀ 𝑣 ∈ 𝑇 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) ) ) |
17 |
16
|
cbvraldva |
⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑇 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) ) ) |
18 |
17
|
rspcev |
⊢ ( ( 𝐴 ∈ 𝑃 ∧ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑇 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) ) → ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ) |
19 |
7 10 18
|
syl2anc |
⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ) |
20 |
1 2 3 4 5 6
|
axtgcont1 |
⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) |
21 |
19 20
|
mpd |
⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) |