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

Theorem eengtrkg 27977
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 6862 . . . . . 6 (𝑁 ∈ β„• β†’ (EEGβ€˜π‘) ∈ V)
2 simpl 484 . . . . . . . . 9 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑁 ∈ β„•)
3 simprl 770 . . . . . . . . . 10 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)))
4 eengbas 27972 . . . . . . . . . . 11 (𝑁 ∈ β„• β†’ (π”Όβ€˜π‘) = (Baseβ€˜(EEGβ€˜π‘)))
54adantr 482 . . . . . . . . . 10 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ (π”Όβ€˜π‘) = (Baseβ€˜(EEGβ€˜π‘)))
63, 5eleqtrrd 2841 . . . . . . . . 9 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ π‘₯ ∈ (π”Όβ€˜π‘))
7 simprr 772 . . . . . . . . . 10 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))
87, 5eleqtrrd 2841 . . . . . . . . 9 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑦 ∈ (π”Όβ€˜π‘))
9 axcgrrflx 27905 . . . . . . . . 9 ((𝑁 ∈ β„• ∧ π‘₯ ∈ (π”Όβ€˜π‘) ∧ 𝑦 ∈ (π”Όβ€˜π‘)) β†’ ⟨π‘₯, π‘¦βŸ©CgrβŸ¨π‘¦, π‘₯⟩)
102, 6, 8, 9syl3anc 1372 . . . . . . . 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 27974 . . . . . . . 8 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ (⟨π‘₯, π‘¦βŸ©CgrβŸ¨π‘¦, π‘₯⟩ ↔ (π‘₯(distβ€˜(EEGβ€˜π‘))𝑦) = (𝑦(distβ€˜(EEGβ€˜π‘))π‘₯)))
1410, 13mpbid 231 . . . . . . 7 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ (π‘₯(distβ€˜(EEGβ€˜π‘))𝑦) = (𝑦(distβ€˜(EEGβ€˜π‘))π‘₯))
1514ralrimivva 3198 . . . . . 6 (𝑁 ∈ β„• β†’ βˆ€π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘¦ ∈ (Baseβ€˜(EEGβ€˜π‘))(π‘₯(distβ€˜(EEGβ€˜π‘))𝑦) = (𝑦(distβ€˜(EEGβ€˜π‘))π‘₯))
16 simpl 484 . . . . . . . . 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 27974 . . . . . . . 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 482 . . . . . . . . . 10 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ (π”Όβ€˜π‘) = (Baseβ€˜(EEGβ€˜π‘)))
2419, 23eleqtrrd 2841 . . . . . . . . 9 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑧 ∈ (π”Όβ€˜π‘))
25 axcgrid 27907 . . . . . . . . 9 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (π”Όβ€˜π‘) ∧ 𝑦 ∈ (π”Όβ€˜π‘) ∧ 𝑧 ∈ (π”Όβ€˜π‘))) β†’ (⟨π‘₯, π‘¦βŸ©CgrβŸ¨π‘§, π‘§βŸ© β†’ π‘₯ = 𝑦))
2616, 21, 22, 24, 25syl13anc 1373 . . . . . . . 8 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ (⟨π‘₯, π‘¦βŸ©CgrβŸ¨π‘§, π‘§βŸ© β†’ π‘₯ = 𝑦))
2720, 26sylbird 260 . . . . . . 7 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ ((π‘₯(distβ€˜(EEGβ€˜π‘))𝑦) = (𝑧(distβ€˜(EEGβ€˜π‘))𝑧) β†’ π‘₯ = 𝑦))
2827ralrimivvva 3201 . . . . . 6 (𝑁 ∈ β„• β†’ βˆ€π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘¦ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘§ ∈ (Baseβ€˜(EEGβ€˜π‘))((π‘₯(distβ€˜(EEGβ€˜π‘))𝑦) = (𝑧(distβ€˜(EEGβ€˜π‘))𝑧) β†’ π‘₯ = 𝑦))
291, 15, 28jca32 517 . . . . 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 27438 . . . . 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 233 . . . 4 (𝑁 ∈ β„• β†’ (EEGβ€˜π‘) ∈ TarskiGC)
332, 11, 30, 3, 3, 7ebtwntg 27973 . . . . . . . . . . 11 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ (𝑦 Btwn ⟨π‘₯, π‘₯⟩ ↔ 𝑦 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))π‘₯)))
34 axbtwnid 27930 . . . . . . . . . . . 12 ((𝑁 ∈ β„• ∧ 𝑦 ∈ (π”Όβ€˜π‘) ∧ π‘₯ ∈ (π”Όβ€˜π‘)) β†’ (𝑦 Btwn ⟨π‘₯, π‘₯⟩ β†’ 𝑦 = π‘₯))
352, 8, 6, 34syl3anc 1372 . . . . . . . . . . 11 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ (𝑦 Btwn ⟨π‘₯, π‘₯⟩ β†’ 𝑦 = π‘₯))
3633, 35sylbird 260 . . . . . . . . . 10 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ (𝑦 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))π‘₯) β†’ 𝑦 = π‘₯))
3736imp 408 . . . . . . . . 9 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑦 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))π‘₯)) β†’ 𝑦 = π‘₯)
3837equcomd 2023 . . . . . . . 8 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑦 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))π‘₯)) β†’ π‘₯ = 𝑦)
3938ex 414 . . . . . . 7 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ (𝑦 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))π‘₯) β†’ π‘₯ = 𝑦))
4039ralrimivva 3198 . . . . . 6 (𝑁 ∈ β„• β†’ βˆ€π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘¦ ∈ (Baseβ€˜(EEGβ€˜π‘))(𝑦 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))π‘₯) β†’ π‘₯ = 𝑦))
41 simpll 766 . . . . . . . . . 10 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑁 ∈ β„•)
426adantr 482 . . . . . . . . . 10 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ π‘₯ ∈ (π”Όβ€˜π‘))
438adantr 482 . . . . . . . . . 10 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑦 ∈ (π”Όβ€˜π‘))
443adantr 482 . . . . . . . . . . 11 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)))
457adantr 482 . . . . . . . . . . 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 1373 . . . . . . . . . 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 2841 . . . . . . . . . 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 2841 . . . . . . . . . 10 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑣 ∈ (π”Όβ€˜π‘))
53 axpasch 27932 . . . . . . . . . 10 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (π”Όβ€˜π‘) ∧ 𝑦 ∈ (π”Όβ€˜π‘) ∧ 𝑧 ∈ (π”Όβ€˜π‘)) ∧ (𝑒 ∈ (π”Όβ€˜π‘) ∧ 𝑣 ∈ (π”Όβ€˜π‘))) β†’ ((𝑒 Btwn ⟨π‘₯, π‘§βŸ© ∧ 𝑣 Btwn βŸ¨π‘¦, π‘§βŸ©) β†’ βˆƒπ‘Ž ∈ (π”Όβ€˜π‘)(π‘Ž Btwn βŸ¨π‘’, π‘¦βŸ© ∧ π‘Ž Btwn βŸ¨π‘£, π‘₯⟩)))
5441, 42, 43, 47, 50, 52, 53syl132anc 1389 . . . . . . . . 9 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ ((𝑒 Btwn ⟨π‘₯, π‘§βŸ© ∧ 𝑣 Btwn βŸ¨π‘¦, π‘§βŸ©) β†’ βˆƒπ‘Ž ∈ (π”Όβ€˜π‘)(π‘Ž Btwn βŸ¨π‘’, π‘¦βŸ© ∧ π‘Ž Btwn βŸ¨π‘£, π‘₯⟩)))
5541, 11, 30, 44, 46, 48ebtwntg 27973 . . . . . . . . . 10 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ (𝑒 Btwn ⟨π‘₯, π‘§βŸ© ↔ 𝑒 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑧)))
5641, 11, 30, 45, 46, 51ebtwntg 27973 . . . . . . . . . 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 774 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) β†’ 𝑁 ∈ β„•)
5948adantr 482 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) β†’ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)))
6045adantr 482 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) β†’ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))
61 simpr 486 . . . . . . . . . . . . 13 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) β†’ π‘Ž ∈ (π”Όβ€˜π‘))
6249adantr 482 . . . . . . . . . . . . 13 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) β†’ (π”Όβ€˜π‘) = (Baseβ€˜(EEGβ€˜π‘)))
6361, 62eleqtrd 2840 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) β†’ π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)))
6458, 11, 30, 59, 60, 63ebtwntg 27973 . . . . . . . . . . 11 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) β†’ (π‘Ž Btwn βŸ¨π‘’, π‘¦βŸ© ↔ π‘Ž ∈ (𝑒(Itvβ€˜(EEGβ€˜π‘))𝑦)))
6551adantr 482 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) β†’ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))
6644adantr 482 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) β†’ π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)))
6758, 11, 30, 65, 66, 63ebtwntg 27973 . . . . . . . . . . 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 3325 . . . . . . . . 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 3201 . . . . . . 7 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ βˆ€π‘§ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘’ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘£ ∈ (Baseβ€˜(EEGβ€˜π‘))((𝑒 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑧) ∧ 𝑣 ∈ (𝑦(Itvβ€˜(EEGβ€˜π‘))𝑧)) β†’ βˆƒπ‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘))(π‘Ž ∈ (𝑒(Itvβ€˜(EEGβ€˜π‘))𝑦) ∧ π‘Ž ∈ (𝑣(Itvβ€˜(EEGβ€˜π‘))π‘₯))))
7271ralrimivva 3198 . . . . . 6 (𝑁 ∈ β„• β†’ βˆ€π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘¦ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘§ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘’ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘£ ∈ (Baseβ€˜(EEGβ€˜π‘))((𝑒 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑧) ∧ 𝑣 ∈ (𝑦(Itvβ€˜(EEGβ€˜π‘))𝑧)) β†’ βˆƒπ‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘))(π‘Ž ∈ (𝑒(Itvβ€˜(EEGβ€˜π‘))𝑦) ∧ π‘Ž ∈ (𝑣(Itvβ€˜(EEGβ€˜π‘))π‘₯))))
73 simpl 484 . . . . . . . . 9 ((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑁 ∈ β„•)
74 elpwi 4572 . . . . . . . . . . 11 (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) β†’ 𝑠 βŠ† (Baseβ€˜(EEGβ€˜π‘)))
7574ad2antrl 727 . . . . . . . . . 10 ((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑠 βŠ† (Baseβ€˜(EEGβ€˜π‘)))
764adantr 482 . . . . . . . . . 10 ((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) β†’ (π”Όβ€˜π‘) = (Baseβ€˜(EEGβ€˜π‘)))
7775, 76sseqtrrd 3990 . . . . . . . . 9 ((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑠 βŠ† (π”Όβ€˜π‘))
78 elpwi 4572 . . . . . . . . . . 11 (𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) β†’ 𝑑 βŠ† (Baseβ€˜(EEGβ€˜π‘)))
7978ad2antll 728 . . . . . . . . . 10 ((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑑 βŠ† (Baseβ€˜(EEGβ€˜π‘)))
8079, 76sseqtrrd 3990 . . . . . . . . 9 ((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑑 βŠ† (π”Όβ€˜π‘))
81 simpll 766 . . . . . . . . . . 11 (((𝑁 ∈ β„• ∧ (𝑠 βŠ† (π”Όβ€˜π‘) ∧ 𝑑 βŠ† (π”Όβ€˜π‘))) ∧ βˆƒπ‘Ž ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ Btwn βŸ¨π‘Ž, π‘¦βŸ©) β†’ 𝑁 ∈ β„•)
82 simplrl 776 . . . . . . . . . . 11 (((𝑁 ∈ β„• ∧ (𝑠 βŠ† (π”Όβ€˜π‘) ∧ 𝑑 βŠ† (π”Όβ€˜π‘))) ∧ βˆƒπ‘Ž ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ Btwn βŸ¨π‘Ž, π‘¦βŸ©) β†’ 𝑠 βŠ† (π”Όβ€˜π‘))
83 simplrr 777 . . . . . . . . . . 11 (((𝑁 ∈ β„• ∧ (𝑠 βŠ† (π”Όβ€˜π‘) ∧ 𝑑 βŠ† (π”Όβ€˜π‘))) ∧ βˆƒπ‘Ž ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ Btwn βŸ¨π‘Ž, π‘¦βŸ©) β†’ 𝑑 βŠ† (π”Όβ€˜π‘))
84 simpr 486 . . . . . . . . . . 11 (((𝑁 ∈ β„• ∧ (𝑠 βŠ† (π”Όβ€˜π‘) ∧ 𝑑 βŠ† (π”Όβ€˜π‘))) ∧ βˆƒπ‘Ž ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ Btwn βŸ¨π‘Ž, π‘¦βŸ©) β†’ βˆƒπ‘Ž ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ Btwn βŸ¨π‘Ž, π‘¦βŸ©)
85 axcont 27967 . . . . . . . . . . 11 ((𝑁 ∈ β„• ∧ (𝑠 βŠ† (π”Όβ€˜π‘) ∧ 𝑑 βŠ† (π”Όβ€˜π‘) ∧ βˆƒπ‘Ž ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ Btwn βŸ¨π‘Ž, π‘¦βŸ©)) β†’ βˆƒπ‘ ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 Btwn ⟨π‘₯, π‘¦βŸ©)
8681, 82, 83, 84, 85syl13anc 1373 . . . . . . . . . 10 (((𝑁 ∈ β„• ∧ (𝑠 βŠ† (π”Όβ€˜π‘) ∧ 𝑑 βŠ† (π”Όβ€˜π‘))) ∧ βˆƒπ‘Ž ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ Btwn βŸ¨π‘Ž, π‘¦βŸ©) β†’ βˆƒπ‘ ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 Btwn ⟨π‘₯, π‘¦βŸ©)
8786ex 414 . . . . . . . . 9 ((𝑁 ∈ β„• ∧ (𝑠 βŠ† (π”Όβ€˜π‘) ∧ 𝑑 βŠ† (π”Όβ€˜π‘))) β†’ (βˆƒπ‘Ž ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ Btwn βŸ¨π‘Ž, π‘¦βŸ© β†’ βˆƒπ‘ ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 Btwn ⟨π‘₯, π‘¦βŸ©))
8873, 77, 80, 87syl12anc 836 . . . . . . . 8 ((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) β†’ (βˆƒπ‘Ž ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ Btwn βŸ¨π‘Ž, π‘¦βŸ© β†’ βˆƒπ‘ ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 Btwn ⟨π‘₯, π‘¦βŸ©))
89 simplll 774 . . . . . . . . . . 11 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑁 ∈ β„•)
90 simplr 768 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘Ž ∈ (π”Όβ€˜π‘))
9176ad2antrr 725 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (π”Όβ€˜π‘) = (Baseβ€˜(EEGβ€˜π‘)))
9290, 91eleqtrd 2840 . . . . . . . . . . 11 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)))
9379ad2antrr 725 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 βŠ† (Baseβ€˜(EEGβ€˜π‘)))
94 simprr 772 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝑑)
9593, 94sseldd 3950 . . . . . . . . . . 11 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))
9675ad2antrr 725 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑠 βŠ† (Baseβ€˜(EEGβ€˜π‘)))
97 simprl 770 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘₯ ∈ 𝑠)
9896, 97sseldd 3950 . . . . . . . . . . 11 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)))
9989, 11, 30, 92, 95, 98ebtwntg 27973 . . . . . . . . . 10 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (π‘₯ Btwn βŸ¨π‘Ž, π‘¦βŸ© ↔ π‘₯ ∈ (π‘Ž(Itvβ€˜(EEGβ€˜π‘))𝑦)))
100992ralbidva 3211 . . . . . . . . 9 (((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ Btwn βŸ¨π‘Ž, π‘¦βŸ© ↔ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Ž(Itvβ€˜(EEGβ€˜π‘))𝑦)))
10176, 100rexeqbidva 3325 . . . . . . . 8 ((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) β†’ (βˆƒπ‘Ž ∈ (π”Όβ€˜π‘)βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ Btwn βŸ¨π‘Ž, π‘¦βŸ© ↔ βˆƒπ‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Ž(Itvβ€˜(EEGβ€˜π‘))𝑦)))
102 simplll 774 . . . . . . . . . . 11 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑏 ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑁 ∈ β„•)
10375ad2antrr 725 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑏 ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑠 βŠ† (Baseβ€˜(EEGβ€˜π‘)))
104 simprl 770 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑏 ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘₯ ∈ 𝑠)
105103, 104sseldd 3950 . . . . . . . . . . 11 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑏 ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)))
10679ad2antrr 725 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑏 ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 βŠ† (Baseβ€˜(EEGβ€˜π‘)))
107 simprr 772 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑏 ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝑑)
108106, 107sseldd 3950 . . . . . . . . . . 11 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑏 ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))
109 simplr 768 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑏 ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑏 ∈ (π”Όβ€˜π‘))
11076ad2antrr 725 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑏 ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (π”Όβ€˜π‘) = (Baseβ€˜(EEGβ€˜π‘)))
111109, 110eleqtrd 2840 . . . . . . . . . . 11 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑏 ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))
112102, 11, 30, 105, 108, 111ebtwntg 27973 . . . . . . . . . 10 ((((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑏 ∈ (π”Όβ€˜π‘)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (𝑏 Btwn ⟨π‘₯, π‘¦βŸ© ↔ 𝑏 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑦)))
1131122ralbidva 3211 . . . . . . . . 9 (((𝑁 ∈ β„• ∧ (𝑠 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑑 ∈ 𝒫 (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑏 ∈ (π”Όβ€˜π‘)) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 Btwn ⟨π‘₯, π‘¦βŸ© ↔ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑦)))
11476, 113rexeqbidva 3325 . . . . . . . 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 3198 . . . . . 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 27439 . . . . 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 584 . . . 4 (𝑁 ∈ β„• β†’ (EEGβ€˜π‘) ∈ TarskiGB)
12032, 119elind 4159 . . 3 (𝑁 ∈ β„• β†’ (EEGβ€˜π‘) ∈ (TarskiGC ∩ TarskiGB))
121 simplll 774 . . . . . . . . . . 11 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑐 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑁 ∈ β„•)
1223ad2antrr 725 . . . . . . . . . . . 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 2841 . . . . . . . . . . 11 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑐 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ π‘₯ ∈ (π”Όβ€˜π‘))
1257ad2antrr 725 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑐 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))
126125, 123eleqtrrd 2841 . . . . . . . . . . 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 2841 . . . . . . . . . . 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 2841 . . . . . . . . . . 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 2841 . . . . . . . . . . 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 2841 . . . . . . . . . . 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 2841 . . . . . . . . . . 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 2841 . . . . . . . . . . 11 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑐 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑣 ∈ (π”Όβ€˜π‘))
139 3anass 1096 . . . . . . . . . . . 12 (((π‘₯ β‰  𝑦 ∧ 𝑦 Btwn ⟨π‘₯, π‘§βŸ© ∧ 𝑏 Btwn βŸ¨π‘Ž, π‘βŸ©) ∧ (⟨π‘₯, π‘¦βŸ©CgrβŸ¨π‘Ž, π‘βŸ© ∧ βŸ¨π‘¦, π‘§βŸ©CgrβŸ¨π‘, π‘βŸ©) ∧ (⟨π‘₯, π‘’βŸ©CgrβŸ¨π‘Ž, π‘£βŸ© ∧ βŸ¨π‘¦, π‘’βŸ©CgrβŸ¨π‘, π‘£βŸ©)) ↔ ((π‘₯ β‰  𝑦 ∧ 𝑦 Btwn ⟨π‘₯, π‘§βŸ© ∧ 𝑏 Btwn βŸ¨π‘Ž, π‘βŸ©) ∧ ((⟨π‘₯, π‘¦βŸ©CgrβŸ¨π‘Ž, π‘βŸ© ∧ βŸ¨π‘¦, π‘§βŸ©CgrβŸ¨π‘, π‘βŸ©) ∧ (⟨π‘₯, π‘’βŸ©CgrβŸ¨π‘Ž, π‘£βŸ© ∧ βŸ¨π‘¦, π‘’βŸ©CgrβŸ¨π‘, π‘£βŸ©))))
140 ax5seg 27929 . . . . . . . . . . . 12 (((𝑁 ∈ β„• ∧ π‘₯ ∈ (π”Όβ€˜π‘) ∧ 𝑦 ∈ (π”Όβ€˜π‘)) ∧ (𝑧 ∈ (π”Όβ€˜π‘) ∧ 𝑒 ∈ (π”Όβ€˜π‘) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) ∧ (𝑏 ∈ (π”Όβ€˜π‘) ∧ 𝑐 ∈ (π”Όβ€˜π‘) ∧ 𝑣 ∈ (π”Όβ€˜π‘))) β†’ (((π‘₯ β‰  𝑦 ∧ 𝑦 Btwn ⟨π‘₯, π‘§βŸ© ∧ 𝑏 Btwn βŸ¨π‘Ž, π‘βŸ©) ∧ (⟨π‘₯, π‘¦βŸ©CgrβŸ¨π‘Ž, π‘βŸ© ∧ βŸ¨π‘¦, π‘§βŸ©CgrβŸ¨π‘, π‘βŸ©) ∧ (⟨π‘₯, π‘’βŸ©CgrβŸ¨π‘Ž, π‘£βŸ© ∧ βŸ¨π‘¦, π‘’βŸ©CgrβŸ¨π‘, π‘£βŸ©)) β†’ βŸ¨π‘§, π‘’βŸ©CgrβŸ¨π‘, π‘£βŸ©))
141139, 140biimtrrid 242 . . . . . . . . . . 11 (((𝑁 ∈ β„• ∧ π‘₯ ∈ (π”Όβ€˜π‘) ∧ 𝑦 ∈ (π”Όβ€˜π‘)) ∧ (𝑧 ∈ (π”Όβ€˜π‘) ∧ 𝑒 ∈ (π”Όβ€˜π‘) ∧ π‘Ž ∈ (π”Όβ€˜π‘)) ∧ (𝑏 ∈ (π”Όβ€˜π‘) ∧ 𝑐 ∈ (π”Όβ€˜π‘) ∧ 𝑣 ∈ (π”Όβ€˜π‘))) β†’ (((π‘₯ β‰  𝑦 ∧ 𝑦 Btwn ⟨π‘₯, π‘§βŸ© ∧ 𝑏 Btwn βŸ¨π‘Ž, π‘βŸ©) ∧ ((⟨π‘₯, π‘¦βŸ©CgrβŸ¨π‘Ž, π‘βŸ© ∧ βŸ¨π‘¦, π‘§βŸ©CgrβŸ¨π‘, π‘βŸ©) ∧ (⟨π‘₯, π‘’βŸ©CgrβŸ¨π‘Ž, π‘£βŸ© ∧ βŸ¨π‘¦, π‘’βŸ©CgrβŸ¨π‘, π‘£βŸ©))) β†’ βŸ¨π‘§, π‘’βŸ©CgrβŸ¨π‘, π‘£βŸ©))
142121, 124, 126, 128, 130, 132, 134, 136, 138, 141syl333anc 1403 . . . . . . . . . 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 27973 . . . . . . . . . . . 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 27973 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑒 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑐 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑣 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ (𝑏 Btwn βŸ¨π‘Ž, π‘βŸ© ↔ 𝑏 ∈ (π‘Ž(Itvβ€˜(EEGβ€˜π‘))𝑐)))
145143, 1443anbi23d 1440 . . . . . . . . . . 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 27974 . . . . . . . . . . . . 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 27974 . . . . . . . . . . . . 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 27974 . . . . . . . . . . . . 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 27974 . . . . . . . . . . . . 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 27974 . . . . . . . . . 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 3201 . . . . . . . 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 3201 . . . . . . 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 3198 . . . . . 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 766 . . . . . . . . . 10 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑁 ∈ β„•)
1606adantr 482 . . . . . . . . . 10 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ π‘₯ ∈ (π”Όβ€˜π‘))
1618adantr 482 . . . . . . . . . 10 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑦 ∈ (π”Όβ€˜π‘))
162 simprl 770 . . . . . . . . . . 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 2841 . . . . . . . . . 10 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ π‘Ž ∈ (π”Όβ€˜π‘))
165 simprr 772 . . . . . . . . . . 11 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))
166165, 163eleqtrrd 2841 . . . . . . . . . 10 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ 𝑏 ∈ (π”Όβ€˜π‘))
167 axsegcon 27918 . . . . . . . . . 10 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (π”Όβ€˜π‘) ∧ 𝑦 ∈ (π”Όβ€˜π‘)) ∧ (π‘Ž ∈ (π”Όβ€˜π‘) ∧ 𝑏 ∈ (π”Όβ€˜π‘))) β†’ βˆƒπ‘§ ∈ (π”Όβ€˜π‘)(𝑦 Btwn ⟨π‘₯, π‘§βŸ© ∧ βŸ¨π‘¦, π‘§βŸ©CgrβŸ¨π‘Ž, π‘βŸ©))
168159, 160, 161, 164, 166, 167syl122anc 1380 . . . . . . . . 9 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ βˆƒπ‘§ ∈ (π”Όβ€˜π‘)(𝑦 Btwn ⟨π‘₯, π‘§βŸ© ∧ βŸ¨π‘¦, π‘§βŸ©CgrβŸ¨π‘Ž, π‘βŸ©))
169 simplll 774 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑧 ∈ (π”Όβ€˜π‘)) β†’ 𝑁 ∈ β„•)
1703ad2antrr 725 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑧 ∈ (π”Όβ€˜π‘)) β†’ π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)))
171 simpr 486 . . . . . . . . . . . . 13 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑧 ∈ (π”Όβ€˜π‘)) β†’ 𝑧 ∈ (π”Όβ€˜π‘))
172163adantr 482 . . . . . . . . . . . . 13 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑧 ∈ (π”Όβ€˜π‘)) β†’ (π”Όβ€˜π‘) = (Baseβ€˜(EEGβ€˜π‘)))
173171, 172eleqtrd 2840 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑧 ∈ (π”Όβ€˜π‘)) β†’ 𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)))
1747ad2antrr 725 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑧 ∈ (π”Όβ€˜π‘)) β†’ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))
175169, 11, 30, 170, 173, 174ebtwntg 27973 . . . . . . . . . . 11 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑧 ∈ (π”Όβ€˜π‘)) β†’ (𝑦 Btwn ⟨π‘₯, π‘§βŸ© ↔ 𝑦 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑧)))
176 simplrl 776 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑧 ∈ (π”Όβ€˜π‘)) β†’ π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)))
177 simplrr 777 . . . . . . . . . . . 12 ((((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ 𝑧 ∈ (π”Όβ€˜π‘)) β†’ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))
178169, 11, 12, 174, 173, 176, 177ecgrtg 27974 . . . . . . . . . . 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 3325 . . . . . . . . 9 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ (βˆƒπ‘§ ∈ (π”Όβ€˜π‘)(𝑦 Btwn ⟨π‘₯, π‘§βŸ© ∧ βŸ¨π‘¦, π‘§βŸ©CgrβŸ¨π‘Ž, π‘βŸ©) ↔ βˆƒπ‘§ ∈ (Baseβ€˜(EEGβ€˜π‘))(𝑦 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑧) ∧ (𝑦(distβ€˜(EEGβ€˜π‘))𝑧) = (π‘Ž(distβ€˜(EEGβ€˜π‘))𝑏))))
181168, 180mpbid 231 . . . . . . . 8 (((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) ∧ (π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑏 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ βˆƒπ‘§ ∈ (Baseβ€˜(EEGβ€˜π‘))(𝑦 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑧) ∧ (𝑦(distβ€˜(EEGβ€˜π‘))𝑧) = (π‘Ž(distβ€˜(EEGβ€˜π‘))𝑏)))
182181ralrimivva 3198 . . . . . . 7 ((𝑁 ∈ β„• ∧ (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(EEGβ€˜π‘)))) β†’ βˆ€π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆƒπ‘§ ∈ (Baseβ€˜(EEGβ€˜π‘))(𝑦 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑧) ∧ (𝑦(distβ€˜(EEGβ€˜π‘))𝑧) = (π‘Ž(distβ€˜(EEGβ€˜π‘))𝑏)))
183182ralrimivva 3198 . . . . . 6 (𝑁 ∈ β„• β†’ βˆ€π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘¦ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘Ž ∈ (Baseβ€˜(EEGβ€˜π‘))βˆ€π‘ ∈ (Baseβ€˜(EEGβ€˜π‘))βˆƒπ‘§ ∈ (Baseβ€˜(EEGβ€˜π‘))(𝑦 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑧) ∧ (𝑦(distβ€˜(EEGβ€˜π‘))𝑧) = (π‘Ž(distβ€˜(EEGβ€˜π‘))𝑏)))
1841, 158, 183jca32 517 . . . . 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 27440 . . . . 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 233 . . . 4 (𝑁 ∈ β„• β†’ (EEGβ€˜π‘) ∈ TarskiGCB)
18711, 30elntg 27975 . . . . 5 (𝑁 ∈ β„• β†’ (LineGβ€˜(EEGβ€˜π‘)) = (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)), 𝑦 ∈ ((Baseβ€˜(EEGβ€˜π‘)) βˆ– {π‘₯}) ↦ {𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∣ (𝑧 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑦) ∨ π‘₯ ∈ (𝑧(Itvβ€˜(EEGβ€˜π‘))𝑦) ∨ 𝑦 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑧))}))
18811, 12, 30istrkgl 27442 . . . . 5 ((EEGβ€˜π‘) ∈ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})} ↔ ((EEGβ€˜π‘) ∈ V ∧ (LineGβ€˜(EEGβ€˜π‘)) = (π‘₯ ∈ (Baseβ€˜(EEGβ€˜π‘)), 𝑦 ∈ ((Baseβ€˜(EEGβ€˜π‘)) βˆ– {π‘₯}) ↦ {𝑧 ∈ (Baseβ€˜(EEGβ€˜π‘)) ∣ (𝑧 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑦) ∨ π‘₯ ∈ (𝑧(Itvβ€˜(EEGβ€˜π‘))𝑦) ∨ 𝑦 ∈ (π‘₯(Itvβ€˜(EEGβ€˜π‘))𝑧))})))
1891, 187, 188sylanbrc 584 . . . 4 (𝑁 ∈ β„• β†’ (EEGβ€˜π‘) ∈ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})
190186, 189elind 4159 . . 3 (𝑁 ∈ β„• β†’ (EEGβ€˜π‘) ∈ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
191120, 190elind 4159 . 2 (𝑁 ∈ β„• β†’ (EEGβ€˜π‘) ∈ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})))
192 df-trkg 27437 . 2 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
193191, 192eleqtrrdi 2849 1 (𝑁 ∈ β„• β†’ (EEGβ€˜π‘) ∈ TarskiG)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∨ w3o 1087   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {cab 2714   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  {crab 3410  Vcvv 3448  [wsbc 3744   βˆ– cdif 3912   ∩ cin 3914   βŠ† wss 3915  π’« cpw 4565  {csn 4591  βŸ¨cop 4597   class class class wbr 5110  β€˜cfv 6501  (class class class)co 7362   ∈ cmpo 7364  β„•cn 12160  Basecbs 17090  distcds 17149  TarskiGcstrkg 27411  TarskiGCcstrkgc 27412  TarskiGBcstrkgb 27413  TarskiGCBcstrkgcb 27414  Itvcitv 27417  LineGclng 27418  π”Όcee 27879   Btwn cbtwn 27880  Cgrccgr 27881  EEGceeng 27968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-rp 12923  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-sum 15578  df-struct 17026  df-slot 17061  df-ndx 17073  df-base 17091  df-ds 17162  df-itv 27419  df-lng 27420  df-trkgc 27432  df-trkgb 27433  df-trkgcb 27434  df-trkg 27437  df-ee 27882  df-btwn 27883  df-cgr 27884  df-eeng 27969
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator