MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eengtrkg Structured version   Visualization version   GIF version

Theorem eengtrkg 29001
Description: The geometry structure for 𝔼↑𝑁 is a Tarski geometry. (Contributed by Thierry Arnoux, 15-Mar-2019.)
Assertion
Ref Expression
eengtrkg (𝑁 ∈ ℕ → (EEG‘𝑁) ∈ TarskiG)

Proof of Theorem eengtrkg
Dummy variables 𝑎 𝑏 𝑐 𝑓 𝑖 𝑝 𝑠 𝑡 𝑢 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvexd 6921 . . . . . 6 (𝑁 ∈ ℕ → (EEG‘𝑁) ∈ V)
2 simpl 482 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ)
3 simprl 771 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (Base‘(EEG‘𝑁)))
4 eengbas 28996 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝔼‘𝑁) = (Base‘(EEG‘𝑁)))
54adantr 480 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁)))
63, 5eleqtrrd 2844 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁))
7 simprr 773 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (Base‘(EEG‘𝑁)))
87, 5eleqtrrd 2844 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁))
9 axcgrrflx 28929 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → ⟨𝑥, 𝑦⟩Cgr⟨𝑦, 𝑥⟩)
102, 6, 8, 9syl3anc 1373 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → ⟨𝑥, 𝑦⟩Cgr⟨𝑦, 𝑥⟩)
11 eqid 2737 . . . . . . . . 9 (Base‘(EEG‘𝑁)) = (Base‘(EEG‘𝑁))
12 eqid 2737 . . . . . . . . 9 (dist‘(EEG‘𝑁)) = (dist‘(EEG‘𝑁))
132, 11, 12, 3, 7, 7, 3ecgrtg 28998 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → (⟨𝑥, 𝑦⟩Cgr⟨𝑦, 𝑥⟩ ↔ (𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑦(dist‘(EEG‘𝑁))𝑥)))
1410, 13mpbid 232 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → (𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑦(dist‘(EEG‘𝑁))𝑥))
1514ralrimivva 3202 . . . . . 6 (𝑁 ∈ ℕ → ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))(𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑦(dist‘(EEG‘𝑁))𝑥))
16 simpl 482 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑧 ∈ (Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ)
17 simpr1 1195 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑧 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (Base‘(EEG‘𝑁)))
18 simpr2 1196 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑧 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (Base‘(EEG‘𝑁)))
19 simpr3 1197 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑧 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (Base‘(EEG‘𝑁)))
2016, 11, 12, 17, 18, 19, 19ecgrtg 28998 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑧 ∈ (Base‘(EEG‘𝑁)))) → (⟨𝑥, 𝑦⟩Cgr⟨𝑧, 𝑧⟩ ↔ (𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑧(dist‘(EEG‘𝑁))𝑧)))
2163adantr3 1172 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑧 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁))
2283adantr3 1172 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑧 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁))
234adantr 480 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑧 ∈ (Base‘(EEG‘𝑁)))) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁)))
2419, 23eleqtrrd 2844 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑧 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (𝔼‘𝑁))
25 axcgrid 28931 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → (⟨𝑥, 𝑦⟩Cgr⟨𝑧, 𝑧⟩ → 𝑥 = 𝑦))
2616, 21, 22, 24, 25syl13anc 1374 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑧 ∈ (Base‘(EEG‘𝑁)))) → (⟨𝑥, 𝑦⟩Cgr⟨𝑧, 𝑧⟩ → 𝑥 = 𝑦))
2720, 26sylbird 260 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑧 ∈ (Base‘(EEG‘𝑁)))) → ((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑧(dist‘(EEG‘𝑁))𝑧) → 𝑥 = 𝑦))
2827ralrimivvva 3205 . . . . . 6 (𝑁 ∈ ℕ → ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑧 ∈ (Base‘(EEG‘𝑁))((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑧(dist‘(EEG‘𝑁))𝑧) → 𝑥 = 𝑦))
291, 15, 28jca32 515 . . . . 5 (𝑁 ∈ ℕ → ((EEG‘𝑁) ∈ V ∧ (∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))(𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑦(dist‘(EEG‘𝑁))𝑥) ∧ ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑧 ∈ (Base‘(EEG‘𝑁))((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑧(dist‘(EEG‘𝑁))𝑧) → 𝑥 = 𝑦))))
30 eqid 2737 . . . . . 6 (Itv‘(EEG‘𝑁)) = (Itv‘(EEG‘𝑁))
3111, 12, 30istrkgc 28462 . . . . 5 ((EEG‘𝑁) ∈ TarskiGC ↔ ((EEG‘𝑁) ∈ V ∧ (∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))(𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑦(dist‘(EEG‘𝑁))𝑥) ∧ ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑧 ∈ (Base‘(EEG‘𝑁))((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑧(dist‘(EEG‘𝑁))𝑧) → 𝑥 = 𝑦))))
3229, 31sylibr 234 . . . 4 (𝑁 ∈ ℕ → (EEG‘𝑁) ∈ TarskiGC)
332, 11, 30, 3, 3, 7ebtwntg 28997 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → (𝑦 Btwn ⟨𝑥, 𝑥⟩ ↔ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥)))
34 axbtwnid 28954 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑦 Btwn ⟨𝑥, 𝑥⟩ → 𝑦 = 𝑥))
352, 8, 6, 34syl3anc 1373 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → (𝑦 Btwn ⟨𝑥, 𝑥⟩ → 𝑦 = 𝑥))
3633, 35sylbird 260 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → (𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥) → 𝑦 = 𝑥))
3736imp 406 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥)) → 𝑦 = 𝑥)
3837equcomd 2018 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥)) → 𝑥 = 𝑦)
3938ex 412 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → (𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥) → 𝑥 = 𝑦))
4039ralrimivva 3202 . . . . . 6 (𝑁 ∈ ℕ → ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥) → 𝑥 = 𝑦))
41 simpll 767 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ)
426adantr 480 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁))
438adantr 480 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁))
443adantr 480 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (Base‘(EEG‘𝑁)))
457adantr 480 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (Base‘(EEG‘𝑁)))
46 simpr1 1195 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (Base‘(EEG‘𝑁)))
4741, 44, 45, 46, 24syl13anc 1374 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (𝔼‘𝑁))
48 simpr2 1196 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑢 ∈ (Base‘(EEG‘𝑁)))
4941, 4syl 17 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁)))
5048, 49eleqtrrd 2844 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑢 ∈ (𝔼‘𝑁))
51 simpr3 1197 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑣 ∈ (Base‘(EEG‘𝑁)))
5251, 49eleqtrrd 2844 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑣 ∈ (𝔼‘𝑁))
53 axpasch 28956 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁)) ∧ (𝑢 ∈ (𝔼‘𝑁) ∧ 𝑣 ∈ (𝔼‘𝑁))) → ((𝑢 Btwn ⟨𝑥, 𝑧⟩ ∧ 𝑣 Btwn ⟨𝑦, 𝑧⟩) → ∃𝑎 ∈ (𝔼‘𝑁)(𝑎 Btwn ⟨𝑢, 𝑦⟩ ∧ 𝑎 Btwn ⟨𝑣, 𝑥⟩)))
5441, 42, 43, 47, 50, 52, 53syl132anc 1390 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((𝑢 Btwn ⟨𝑥, 𝑧⟩ ∧ 𝑣 Btwn ⟨𝑦, 𝑧⟩) → ∃𝑎 ∈ (𝔼‘𝑁)(𝑎 Btwn ⟨𝑢, 𝑦⟩ ∧ 𝑎 Btwn ⟨𝑣, 𝑥⟩)))
5541, 11, 30, 44, 46, 48ebtwntg 28997 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝑢 Btwn ⟨𝑥, 𝑧⟩ ↔ 𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧)))
5641, 11, 30, 45, 46, 51ebtwntg 28997 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝑣 Btwn ⟨𝑦, 𝑧⟩ ↔ 𝑣 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧)))
5755, 56anbi12d 632 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((𝑢 Btwn ⟨𝑥, 𝑧⟩ ∧ 𝑣 Btwn ⟨𝑦, 𝑧⟩) ↔ (𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑣 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧))))
58 simplll 775 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
5948adantr 480 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑢 ∈ (Base‘(EEG‘𝑁)))
6045adantr 480 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑦 ∈ (Base‘(EEG‘𝑁)))
61 simpr 484 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑎 ∈ (𝔼‘𝑁))
6249adantr 480 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁)))
6361, 62eleqtrd 2843 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑎 ∈ (Base‘(EEG‘𝑁)))
6458, 11, 30, 59, 60, 63ebtwntg 28997 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → (𝑎 Btwn ⟨𝑢, 𝑦⟩ ↔ 𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦)))
6551adantr 480 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑣 ∈ (Base‘(EEG‘𝑁)))
6644adantr 480 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (Base‘(EEG‘𝑁)))
6758, 11, 30, 65, 66, 63ebtwntg 28997 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → (𝑎 Btwn ⟨𝑣, 𝑥⟩ ↔ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥)))
6864, 67anbi12d 632 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → ((𝑎 Btwn ⟨𝑢, 𝑦⟩ ∧ 𝑎 Btwn ⟨𝑣, 𝑥⟩) ↔ (𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦) ∧ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥))))
6949, 68rexeqbidva 3333 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (∃𝑎 ∈ (𝔼‘𝑁)(𝑎 Btwn ⟨𝑢, 𝑦⟩ ∧ 𝑎 Btwn ⟨𝑣, 𝑥⟩) ↔ ∃𝑎 ∈ (Base‘(EEG‘𝑁))(𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦) ∧ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥))))
7054, 57, 693imtr3d 293 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑣 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧)) → ∃𝑎 ∈ (Base‘(EEG‘𝑁))(𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦) ∧ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥))))
7170ralrimivvva 3205 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → ∀𝑧 ∈ (Base‘(EEG‘𝑁))∀𝑢 ∈ (Base‘(EEG‘𝑁))∀𝑣 ∈ (Base‘(EEG‘𝑁))((𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑣 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧)) → ∃𝑎 ∈ (Base‘(EEG‘𝑁))(𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦) ∧ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥))))
7271ralrimivva 3202 . . . . . 6 (𝑁 ∈ ℕ → ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑧 ∈ (Base‘(EEG‘𝑁))∀𝑢 ∈ (Base‘(EEG‘𝑁))∀𝑣 ∈ (Base‘(EEG‘𝑁))((𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑣 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧)) → ∃𝑎 ∈ (Base‘(EEG‘𝑁))(𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦) ∧ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥))))
73 simpl 482 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ)
74 elpwi 4607 . . . . . . . . . . 11 (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) → 𝑠 ⊆ (Base‘(EEG‘𝑁)))
7574ad2antrl 728 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) → 𝑠 ⊆ (Base‘(EEG‘𝑁)))
764adantr 480 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁)))
7775, 76sseqtrrd 4021 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) → 𝑠 ⊆ (𝔼‘𝑁))
78 elpwi 4607 . . . . . . . . . . 11 (𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)) → 𝑡 ⊆ (Base‘(EEG‘𝑁)))
7978ad2antll 729 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) → 𝑡 ⊆ (Base‘(EEG‘𝑁)))
8079, 76sseqtrrd 4021 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) → 𝑡 ⊆ (𝔼‘𝑁))
81 simpll 767 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁))) ∧ ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑥 Btwn ⟨𝑎, 𝑦⟩) → 𝑁 ∈ ℕ)
82 simplrl 777 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁))) ∧ ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑥 Btwn ⟨𝑎, 𝑦⟩) → 𝑠 ⊆ (𝔼‘𝑁))
83 simplrr 778 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁))) ∧ ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑥 Btwn ⟨𝑎, 𝑦⟩) → 𝑡 ⊆ (𝔼‘𝑁))
84 simpr 484 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁))) ∧ ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑥 Btwn ⟨𝑎, 𝑦⟩) → ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑥 Btwn ⟨𝑎, 𝑦⟩)
85 axcont 28991 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁) ∧ ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑥 Btwn ⟨𝑎, 𝑦⟩)) → ∃𝑏 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑏 Btwn ⟨𝑥, 𝑦⟩)
8681, 82, 83, 84, 85syl13anc 1374 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁))) ∧ ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑥 Btwn ⟨𝑎, 𝑦⟩) → ∃𝑏 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑏 Btwn ⟨𝑥, 𝑦⟩)
8786ex 412 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁))) → (∃𝑎 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑥 Btwn ⟨𝑎, 𝑦⟩ → ∃𝑏 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑏 Btwn ⟨𝑥, 𝑦⟩))
8873, 77, 80, 87syl12anc 837 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) → (∃𝑎 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑥 Btwn ⟨𝑎, 𝑦⟩ → ∃𝑏 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑏 Btwn ⟨𝑥, 𝑦⟩))
89 simplll 775 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑁 ∈ ℕ)
90 simplr 769 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑎 ∈ (𝔼‘𝑁))
9176ad2antrr 726 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁)))
9290, 91eleqtrd 2843 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑎 ∈ (Base‘(EEG‘𝑁)))
9379ad2antrr 726 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡 ⊆ (Base‘(EEG‘𝑁)))
94 simprr 773 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝑡)
9593, 94sseldd 3984 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦 ∈ (Base‘(EEG‘𝑁)))
9675ad2antrr 726 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠 ⊆ (Base‘(EEG‘𝑁)))
97 simprl 771 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝑠)
9896, 97sseldd 3984 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥 ∈ (Base‘(EEG‘𝑁)))
9989, 11, 30, 92, 95, 98ebtwntg 28997 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → (𝑥 Btwn ⟨𝑎, 𝑦⟩ ↔ 𝑥 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑦)))
100992ralbidva 3219 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → (∀𝑥𝑠𝑦𝑡 𝑥 Btwn ⟨𝑎, 𝑦⟩ ↔ ∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑦)))
10176, 100rexeqbidva 3333 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) → (∃𝑎 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑥 Btwn ⟨𝑎, 𝑦⟩ ↔ ∃𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑦)))
102 simplll 775 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑁 ∈ ℕ)
10375ad2antrr 726 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑠 ⊆ (Base‘(EEG‘𝑁)))
104 simprl 771 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥𝑠)
105103, 104sseldd 3984 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑥 ∈ (Base‘(EEG‘𝑁)))
10679ad2antrr 726 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑡 ⊆ (Base‘(EEG‘𝑁)))
107 simprr 773 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦𝑡)
108106, 107sseldd 3984 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑦 ∈ (Base‘(EEG‘𝑁)))
109 simplr 769 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑏 ∈ (𝔼‘𝑁))
11076ad2antrr 726 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁)))
111109, 110eleqtrd 2843 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → 𝑏 ∈ (Base‘(EEG‘𝑁)))
112102, 11, 30, 105, 108, 111ebtwntg 28997 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥𝑠𝑦𝑡)) → (𝑏 Btwn ⟨𝑥, 𝑦⟩ ↔ 𝑏 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦)))
1131122ralbidva 3219 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (∀𝑥𝑠𝑦𝑡 𝑏 Btwn ⟨𝑥, 𝑦⟩ ↔ ∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦)))
11476, 113rexeqbidva 3333 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) → (∃𝑏 ∈ (𝔼‘𝑁)∀𝑥𝑠𝑦𝑡 𝑏 Btwn ⟨𝑥, 𝑦⟩ ↔ ∃𝑏 ∈ (Base‘(EEG‘𝑁))∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦)))
11588, 101, 1143imtr3d 293 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁)) ∧ 𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁)))) → (∃𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑦) → ∃𝑏 ∈ (Base‘(EEG‘𝑁))∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦)))
116115ralrimivva 3202 . . . . . 6 (𝑁 ∈ ℕ → ∀𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁))∀𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁))(∃𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑦) → ∃𝑏 ∈ (Base‘(EEG‘𝑁))∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦)))
11740, 72, 1163jca 1129 . . . . 5 (𝑁 ∈ ℕ → (∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑧 ∈ (Base‘(EEG‘𝑁))∀𝑢 ∈ (Base‘(EEG‘𝑁))∀𝑣 ∈ (Base‘(EEG‘𝑁))((𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑣 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧)) → ∃𝑎 ∈ (Base‘(EEG‘𝑁))(𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦) ∧ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥))) ∧ ∀𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁))∀𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁))(∃𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑦) → ∃𝑏 ∈ (Base‘(EEG‘𝑁))∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦))))
11811, 12, 30istrkgb 28463 . . . . 5 ((EEG‘𝑁) ∈ TarskiGB ↔ ((EEG‘𝑁) ∈ V ∧ (∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑧 ∈ (Base‘(EEG‘𝑁))∀𝑢 ∈ (Base‘(EEG‘𝑁))∀𝑣 ∈ (Base‘(EEG‘𝑁))((𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑣 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧)) → ∃𝑎 ∈ (Base‘(EEG‘𝑁))(𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦) ∧ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥))) ∧ ∀𝑠 ∈ 𝒫 (Base‘(EEG‘𝑁))∀𝑡 ∈ 𝒫 (Base‘(EEG‘𝑁))(∃𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑦) → ∃𝑏 ∈ (Base‘(EEG‘𝑁))∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦)))))
1191, 117, 118sylanbrc 583 . . . 4 (𝑁 ∈ ℕ → (EEG‘𝑁) ∈ TarskiGB)
12032, 119elind 4200 . . 3 (𝑁 ∈ ℕ → (EEG‘𝑁) ∈ (TarskiGC ∩ TarskiGB))
121 simplll 775 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ)
1223ad2antrr 726 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (Base‘(EEG‘𝑁)))
123121, 4syl 17 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁)))
124122, 123eleqtrrd 2844 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁))
1257ad2antrr 726 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (Base‘(EEG‘𝑁)))
126125, 123eleqtrrd 2844 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁))
127 simplr1 1216 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (Base‘(EEG‘𝑁)))
128127, 123eleqtrrd 2844 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (𝔼‘𝑁))
129 simplr2 1217 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑢 ∈ (Base‘(EEG‘𝑁)))
130129, 123eleqtrrd 2844 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑢 ∈ (𝔼‘𝑁))
131 simplr3 1218 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑎 ∈ (Base‘(EEG‘𝑁)))
132131, 123eleqtrrd 2844 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑎 ∈ (𝔼‘𝑁))
133 simpr1 1195 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑏 ∈ (Base‘(EEG‘𝑁)))
134133, 123eleqtrrd 2844 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑏 ∈ (𝔼‘𝑁))
135 simpr2 1196 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑐 ∈ (Base‘(EEG‘𝑁)))
136135, 123eleqtrrd 2844 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑐 ∈ (𝔼‘𝑁))
137 simpr3 1197 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑣 ∈ (Base‘(EEG‘𝑁)))
138137, 123eleqtrrd 2844 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑣 ∈ (𝔼‘𝑁))
139 3anass 1095 . . . . . . . . . . . 12 (((𝑥𝑦𝑦 Btwn ⟨𝑥, 𝑧⟩ ∧ 𝑏 Btwn ⟨𝑎, 𝑐⟩) ∧ (⟨𝑥, 𝑦⟩Cgr⟨𝑎, 𝑏⟩ ∧ ⟨𝑦, 𝑧⟩Cgr⟨𝑏, 𝑐⟩) ∧ (⟨𝑥, 𝑢⟩Cgr⟨𝑎, 𝑣⟩ ∧ ⟨𝑦, 𝑢⟩Cgr⟨𝑏, 𝑣⟩)) ↔ ((𝑥𝑦𝑦 Btwn ⟨𝑥, 𝑧⟩ ∧ 𝑏 Btwn ⟨𝑎, 𝑐⟩) ∧ ((⟨𝑥, 𝑦⟩Cgr⟨𝑎, 𝑏⟩ ∧ ⟨𝑦, 𝑧⟩Cgr⟨𝑏, 𝑐⟩) ∧ (⟨𝑥, 𝑢⟩Cgr⟨𝑎, 𝑣⟩ ∧ ⟨𝑦, 𝑢⟩Cgr⟨𝑏, 𝑣⟩))))
140 ax5seg 28953 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑧 ∈ (𝔼‘𝑁) ∧ 𝑢 ∈ (𝔼‘𝑁) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁) ∧ 𝑣 ∈ (𝔼‘𝑁))) → (((𝑥𝑦𝑦 Btwn ⟨𝑥, 𝑧⟩ ∧ 𝑏 Btwn ⟨𝑎, 𝑐⟩) ∧ (⟨𝑥, 𝑦⟩Cgr⟨𝑎, 𝑏⟩ ∧ ⟨𝑦, 𝑧⟩Cgr⟨𝑏, 𝑐⟩) ∧ (⟨𝑥, 𝑢⟩Cgr⟨𝑎, 𝑣⟩ ∧ ⟨𝑦, 𝑢⟩Cgr⟨𝑏, 𝑣⟩)) → ⟨𝑧, 𝑢⟩Cgr⟨𝑐, 𝑣⟩))
141139, 140biimtrrid 243 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑧 ∈ (𝔼‘𝑁) ∧ 𝑢 ∈ (𝔼‘𝑁) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁) ∧ 𝑣 ∈ (𝔼‘𝑁))) → (((𝑥𝑦𝑦 Btwn ⟨𝑥, 𝑧⟩ ∧ 𝑏 Btwn ⟨𝑎, 𝑐⟩) ∧ ((⟨𝑥, 𝑦⟩Cgr⟨𝑎, 𝑏⟩ ∧ ⟨𝑦, 𝑧⟩Cgr⟨𝑏, 𝑐⟩) ∧ (⟨𝑥, 𝑢⟩Cgr⟨𝑎, 𝑣⟩ ∧ ⟨𝑦, 𝑢⟩Cgr⟨𝑏, 𝑣⟩))) → ⟨𝑧, 𝑢⟩Cgr⟨𝑐, 𝑣⟩))
142121, 124, 126, 128, 130, 132, 134, 136, 138, 141syl333anc 1404 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (((𝑥𝑦𝑦 Btwn ⟨𝑥, 𝑧⟩ ∧ 𝑏 Btwn ⟨𝑎, 𝑐⟩) ∧ ((⟨𝑥, 𝑦⟩Cgr⟨𝑎, 𝑏⟩ ∧ ⟨𝑦, 𝑧⟩Cgr⟨𝑏, 𝑐⟩) ∧ (⟨𝑥, 𝑢⟩Cgr⟨𝑎, 𝑣⟩ ∧ ⟨𝑦, 𝑢⟩Cgr⟨𝑏, 𝑣⟩))) → ⟨𝑧, 𝑢⟩Cgr⟨𝑐, 𝑣⟩))
143121, 11, 30, 122, 127, 125ebtwntg 28997 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝑦 Btwn ⟨𝑥, 𝑧⟩ ↔ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧)))
144121, 11, 30, 131, 135, 133ebtwntg 28997 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝑏 Btwn ⟨𝑎, 𝑐⟩ ↔ 𝑏 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑐)))
145143, 1443anbi23d 1441 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((𝑥𝑦𝑦 Btwn ⟨𝑥, 𝑧⟩ ∧ 𝑏 Btwn ⟨𝑎, 𝑐⟩) ↔ (𝑥𝑦𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑏 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑐))))
146121, 11, 12, 122, 125, 131, 133ecgrtg 28998 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (⟨𝑥, 𝑦⟩Cgr⟨𝑎, 𝑏⟩ ↔ (𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑎(dist‘(EEG‘𝑁))𝑏)))
147121, 11, 12, 125, 127, 133, 135ecgrtg 28998 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (⟨𝑦, 𝑧⟩Cgr⟨𝑏, 𝑐⟩ ↔ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑏(dist‘(EEG‘𝑁))𝑐)))
148146, 147anbi12d 632 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((⟨𝑥, 𝑦⟩Cgr⟨𝑎, 𝑏⟩ ∧ ⟨𝑦, 𝑧⟩Cgr⟨𝑏, 𝑐⟩) ↔ ((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑎(dist‘(EEG‘𝑁))𝑏) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑏(dist‘(EEG‘𝑁))𝑐))))
149121, 11, 12, 122, 129, 131, 137ecgrtg 28998 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (⟨𝑥, 𝑢⟩Cgr⟨𝑎, 𝑣⟩ ↔ (𝑥(dist‘(EEG‘𝑁))𝑢) = (𝑎(dist‘(EEG‘𝑁))𝑣)))
150121, 11, 12, 125, 129, 133, 137ecgrtg 28998 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (⟨𝑦, 𝑢⟩Cgr⟨𝑏, 𝑣⟩ ↔ (𝑦(dist‘(EEG‘𝑁))𝑢) = (𝑏(dist‘(EEG‘𝑁))𝑣)))
151149, 150anbi12d 632 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((⟨𝑥, 𝑢⟩Cgr⟨𝑎, 𝑣⟩ ∧ ⟨𝑦, 𝑢⟩Cgr⟨𝑏, 𝑣⟩) ↔ ((𝑥(dist‘(EEG‘𝑁))𝑢) = (𝑎(dist‘(EEG‘𝑁))𝑣) ∧ (𝑦(dist‘(EEG‘𝑁))𝑢) = (𝑏(dist‘(EEG‘𝑁))𝑣))))
152148, 151anbi12d 632 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (((⟨𝑥, 𝑦⟩Cgr⟨𝑎, 𝑏⟩ ∧ ⟨𝑦, 𝑧⟩Cgr⟨𝑏, 𝑐⟩) ∧ (⟨𝑥, 𝑢⟩Cgr⟨𝑎, 𝑣⟩ ∧ ⟨𝑦, 𝑢⟩Cgr⟨𝑏, 𝑣⟩)) ↔ (((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑎(dist‘(EEG‘𝑁))𝑏) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑏(dist‘(EEG‘𝑁))𝑐)) ∧ ((𝑥(dist‘(EEG‘𝑁))𝑢) = (𝑎(dist‘(EEG‘𝑁))𝑣) ∧ (𝑦(dist‘(EEG‘𝑁))𝑢) = (𝑏(dist‘(EEG‘𝑁))𝑣)))))
153145, 152anbi12d 632 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (((𝑥𝑦𝑦 Btwn ⟨𝑥, 𝑧⟩ ∧ 𝑏 Btwn ⟨𝑎, 𝑐⟩) ∧ ((⟨𝑥, 𝑦⟩Cgr⟨𝑎, 𝑏⟩ ∧ ⟨𝑦, 𝑧⟩Cgr⟨𝑏, 𝑐⟩) ∧ (⟨𝑥, 𝑢⟩Cgr⟨𝑎, 𝑣⟩ ∧ ⟨𝑦, 𝑢⟩Cgr⟨𝑏, 𝑣⟩))) ↔ ((𝑥𝑦𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑏 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑐)) ∧ (((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑎(dist‘(EEG‘𝑁))𝑏) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑏(dist‘(EEG‘𝑁))𝑐)) ∧ ((𝑥(dist‘(EEG‘𝑁))𝑢) = (𝑎(dist‘(EEG‘𝑁))𝑣) ∧ (𝑦(dist‘(EEG‘𝑁))𝑢) = (𝑏(dist‘(EEG‘𝑁))𝑣))))))
154121, 11, 12, 127, 129, 135, 137ecgrtg 28998 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (⟨𝑧, 𝑢⟩Cgr⟨𝑐, 𝑣⟩ ↔ (𝑧(dist‘(EEG‘𝑁))𝑢) = (𝑐(dist‘(EEG‘𝑁))𝑣)))
155142, 153, 1543imtr3d 293 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (((𝑥𝑦𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑏 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑐)) ∧ (((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑎(dist‘(EEG‘𝑁))𝑏) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑏(dist‘(EEG‘𝑁))𝑐)) ∧ ((𝑥(dist‘(EEG‘𝑁))𝑢) = (𝑎(dist‘(EEG‘𝑁))𝑣) ∧ (𝑦(dist‘(EEG‘𝑁))𝑢) = (𝑏(dist‘(EEG‘𝑁))𝑣)))) → (𝑧(dist‘(EEG‘𝑁))𝑢) = (𝑐(dist‘(EEG‘𝑁))𝑣)))
156155ralrimivvva 3205 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) → ∀𝑏 ∈ (Base‘(EEG‘𝑁))∀𝑐 ∈ (Base‘(EEG‘𝑁))∀𝑣 ∈ (Base‘(EEG‘𝑁))(((𝑥𝑦𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑏 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑐)) ∧ (((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑎(dist‘(EEG‘𝑁))𝑏) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑏(dist‘(EEG‘𝑁))𝑐)) ∧ ((𝑥(dist‘(EEG‘𝑁))𝑢) = (𝑎(dist‘(EEG‘𝑁))𝑣) ∧ (𝑦(dist‘(EEG‘𝑁))𝑢) = (𝑏(dist‘(EEG‘𝑁))𝑣)))) → (𝑧(dist‘(EEG‘𝑁))𝑢) = (𝑐(dist‘(EEG‘𝑁))𝑣)))
157156ralrimivvva 3205 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → ∀𝑧 ∈ (Base‘(EEG‘𝑁))∀𝑢 ∈ (Base‘(EEG‘𝑁))∀𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑏 ∈ (Base‘(EEG‘𝑁))∀𝑐 ∈ (Base‘(EEG‘𝑁))∀𝑣 ∈ (Base‘(EEG‘𝑁))(((𝑥𝑦𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑏 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑐)) ∧ (((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑎(dist‘(EEG‘𝑁))𝑏) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑏(dist‘(EEG‘𝑁))𝑐)) ∧ ((𝑥(dist‘(EEG‘𝑁))𝑢) = (𝑎(dist‘(EEG‘𝑁))𝑣) ∧ (𝑦(dist‘(EEG‘𝑁))𝑢) = (𝑏(dist‘(EEG‘𝑁))𝑣)))) → (𝑧(dist‘(EEG‘𝑁))𝑢) = (𝑐(dist‘(EEG‘𝑁))𝑣)))
158157ralrimivva 3202 . . . . . 6 (𝑁 ∈ ℕ → ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑧 ∈ (Base‘(EEG‘𝑁))∀𝑢 ∈ (Base‘(EEG‘𝑁))∀𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑏 ∈ (Base‘(EEG‘𝑁))∀𝑐 ∈ (Base‘(EEG‘𝑁))∀𝑣 ∈ (Base‘(EEG‘𝑁))(((𝑥𝑦𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑏 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑐)) ∧ (((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑎(dist‘(EEG‘𝑁))𝑏) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑏(dist‘(EEG‘𝑁))𝑐)) ∧ ((𝑥(dist‘(EEG‘𝑁))𝑢) = (𝑎(dist‘(EEG‘𝑁))𝑣) ∧ (𝑦(dist‘(EEG‘𝑁))𝑢) = (𝑏(dist‘(EEG‘𝑁))𝑣)))) → (𝑧(dist‘(EEG‘𝑁))𝑢) = (𝑐(dist‘(EEG‘𝑁))𝑣)))
159 simpll 767 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ)
1606adantr 480 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁))
1618adantr 480 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁))
162 simprl 771 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑎 ∈ (Base‘(EEG‘𝑁)))
163159, 4syl 17 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁)))
164162, 163eleqtrrd 2844 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑎 ∈ (𝔼‘𝑁))
165 simprr 773 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑏 ∈ (Base‘(EEG‘𝑁)))
166165, 163eleqtrrd 2844 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑏 ∈ (𝔼‘𝑁))
167 axsegcon 28942 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑎 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁))) → ∃𝑧 ∈ (𝔼‘𝑁)(𝑦 Btwn ⟨𝑥, 𝑧⟩ ∧ ⟨𝑦, 𝑧⟩Cgr⟨𝑎, 𝑏⟩))
168159, 160, 161, 164, 166, 167syl122anc 1381 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → ∃𝑧 ∈ (𝔼‘𝑁)(𝑦 Btwn ⟨𝑥, 𝑧⟩ ∧ ⟨𝑦, 𝑧⟩Cgr⟨𝑎, 𝑏⟩))
169 simplll 775 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
1703ad2antrr 726 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (Base‘(EEG‘𝑁)))
171 simpr 484 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑧 ∈ (𝔼‘𝑁))
172163adantr 480 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁)))
173171, 172eleqtrd 2843 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑧 ∈ (Base‘(EEG‘𝑁)))
1747ad2antrr 726 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑦 ∈ (Base‘(EEG‘𝑁)))
175169, 11, 30, 170, 173, 174ebtwntg 28997 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → (𝑦 Btwn ⟨𝑥, 𝑧⟩ ↔ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧)))
176 simplrl 777 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑎 ∈ (Base‘(EEG‘𝑁)))
177 simplrr 778 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑏 ∈ (Base‘(EEG‘𝑁)))
178169, 11, 12, 174, 173, 176, 177ecgrtg 28998 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → (⟨𝑦, 𝑧⟩Cgr⟨𝑎, 𝑏⟩ ↔ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏)))
179175, 178anbi12d 632 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → ((𝑦 Btwn ⟨𝑥, 𝑧⟩ ∧ ⟨𝑦, 𝑧⟩Cgr⟨𝑎, 𝑏⟩) ↔ (𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏))))
180163, 179rexeqbidva 3333 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → (∃𝑧 ∈ (𝔼‘𝑁)(𝑦 Btwn ⟨𝑥, 𝑧⟩ ∧ ⟨𝑦, 𝑧⟩Cgr⟨𝑎, 𝑏⟩) ↔ ∃𝑧 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏))))
181168, 180mpbid 232 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → ∃𝑧 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏)))
182181ralrimivva 3202 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑦 ∈ (Base‘(EEG‘𝑁)))) → ∀𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑏 ∈ (Base‘(EEG‘𝑁))∃𝑧 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏)))
183182ralrimivva 3202 . . . . . 6 (𝑁 ∈ ℕ → ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑏 ∈ (Base‘(EEG‘𝑁))∃𝑧 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏)))
1841, 158, 183jca32 515 . . . . 5 (𝑁 ∈ ℕ → ((EEG‘𝑁) ∈ V ∧ (∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑧 ∈ (Base‘(EEG‘𝑁))∀𝑢 ∈ (Base‘(EEG‘𝑁))∀𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑏 ∈ (Base‘(EEG‘𝑁))∀𝑐 ∈ (Base‘(EEG‘𝑁))∀𝑣 ∈ (Base‘(EEG‘𝑁))(((𝑥𝑦𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑏 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑐)) ∧ (((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑎(dist‘(EEG‘𝑁))𝑏) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑏(dist‘(EEG‘𝑁))𝑐)) ∧ ((𝑥(dist‘(EEG‘𝑁))𝑢) = (𝑎(dist‘(EEG‘𝑁))𝑣) ∧ (𝑦(dist‘(EEG‘𝑁))𝑢) = (𝑏(dist‘(EEG‘𝑁))𝑣)))) → (𝑧(dist‘(EEG‘𝑁))𝑢) = (𝑐(dist‘(EEG‘𝑁))𝑣)) ∧ ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑏 ∈ (Base‘(EEG‘𝑁))∃𝑧 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏)))))
18511, 12, 30istrkgcb 28464 . . . . 5 ((EEG‘𝑁) ∈ TarskiGCB ↔ ((EEG‘𝑁) ∈ V ∧ (∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑧 ∈ (Base‘(EEG‘𝑁))∀𝑢 ∈ (Base‘(EEG‘𝑁))∀𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑏 ∈ (Base‘(EEG‘𝑁))∀𝑐 ∈ (Base‘(EEG‘𝑁))∀𝑣 ∈ (Base‘(EEG‘𝑁))(((𝑥𝑦𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑏 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑐)) ∧ (((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑎(dist‘(EEG‘𝑁))𝑏) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑏(dist‘(EEG‘𝑁))𝑐)) ∧ ((𝑥(dist‘(EEG‘𝑁))𝑢) = (𝑎(dist‘(EEG‘𝑁))𝑣) ∧ (𝑦(dist‘(EEG‘𝑁))𝑢) = (𝑏(dist‘(EEG‘𝑁))𝑣)))) → (𝑧(dist‘(EEG‘𝑁))𝑢) = (𝑐(dist‘(EEG‘𝑁))𝑣)) ∧ ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑏 ∈ (Base‘(EEG‘𝑁))∃𝑧 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏)))))
186184, 185sylibr 234 . . . 4 (𝑁 ∈ ℕ → (EEG‘𝑁) ∈ TarskiGCB)
18711, 30elntg 28999 . . . . 5 (𝑁 ∈ ℕ → (LineG‘(EEG‘𝑁)) = (𝑥 ∈ (Base‘(EEG‘𝑁)), 𝑦 ∈ ((Base‘(EEG‘𝑁)) ∖ {𝑥}) ↦ {𝑧 ∈ (Base‘(EEG‘𝑁)) ∣ (𝑧 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧))}))
18811, 12, 30istrkgl 28466 . . . . 5 ((EEG‘𝑁) ∈ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ ((EEG‘𝑁) ∈ V ∧ (LineG‘(EEG‘𝑁)) = (𝑥 ∈ (Base‘(EEG‘𝑁)), 𝑦 ∈ ((Base‘(EEG‘𝑁)) ∖ {𝑥}) ↦ {𝑧 ∈ (Base‘(EEG‘𝑁)) ∣ (𝑧 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧))})))
1891, 187, 188sylanbrc 583 . . . 4 (𝑁 ∈ ℕ → (EEG‘𝑁) ∈ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
190186, 189elind 4200 . . 3 (𝑁 ∈ ℕ → (EEG‘𝑁) ∈ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
191120, 190elind 4200 . 2 (𝑁 ∈ ℕ → (EEG‘𝑁) ∈ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})))
192 df-trkg 28461 . 2 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
193191, 192eleqtrrdi 2852 1 (𝑁 ∈ ℕ → (EEG‘𝑁) ∈ TarskiG)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3o 1086  w3a 1087   = wceq 1540  wcel 2108  {cab 2714  wne 2940  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  [wsbc 3788  cdif 3948  cin 3950  wss 3951  𝒫 cpw 4600  {csn 4626  cop 4632   class class class wbr 5143  cfv 6561  (class class class)co 7431  cmpo 7433  cn 12266  Basecbs 17247  distcds 17306  TarskiGcstrkg 28435  TarskiGCcstrkgc 28436  TarskiGBcstrkgb 28437  TarskiGCBcstrkgcb 28438  Itvcitv 28441  LineGclng 28442  𝔼cee 28903   Btwn cbtwn 28904  Cgrccgr 28905  EEGceeng 28992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-rp 13035  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-struct 17184  df-slot 17219  df-ndx 17231  df-base 17248  df-ds 17319  df-itv 28443  df-lng 28444  df-trkgc 28456  df-trkgb 28457  df-trkgcb 28458  df-trkg 28461  df-ee 28906  df-btwn 28907  df-cgr 28908  df-eeng 28993
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator