Metamath Proof Explorer

Theorem istrkgb

Description: Property of being a Tarski geometry - betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019)

Ref Expression
Hypotheses istrkg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
istrkg.d ⊢ − = ( dist ‘ 𝐺 )
istrkg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
Assertion istrkgb ( 𝐺 ∈ TarskiGB ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 istrkg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 istrkg.d ⊢ − = ( dist ‘ 𝐺 )
3 istrkg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 simpl ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → 𝑝 = 𝑃 )
5 4 eqcomd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → 𝑃 = 𝑝 )
6 5 adantr ⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) → 𝑃 = 𝑝 )
7 simpllr ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → 𝑖 = 𝐼 )
8 7 eqcomd ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → 𝐼 = 𝑖 )
9 8 oveqd ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( 𝑥 𝐼 𝑥 ) = ( 𝑥 𝑖 𝑥 ) )
10 9 eleq2d ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) ↔ 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) ) )
11 10 imbi1d ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ↔ ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) → 𝑥 = 𝑦 ) ) )
12 6 11 raleqbidva ⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) → ( ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) → 𝑥 = 𝑦 ) ) )
13 5 12 raleqbidva ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) → 𝑥 = 𝑦 ) ) )
14 6 adantr ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → 𝑃 = 𝑝 )
15 14 adantr ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → 𝑃 = 𝑝 )
16 15 adantr ⊢ ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) → 𝑃 = 𝑝 )
17 simp-6r ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → 𝑖 = 𝐼 )
18 17 eqcomd ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → 𝐼 = 𝑖 )
19 18 oveqd ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑥 𝐼 𝑧 ) = ( 𝑥 𝑖 𝑧 ) )
20 19 eleq2d ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ) )
21 18 oveqd ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑦 𝐼 𝑧 ) = ( 𝑦 𝑖 𝑧 ) )
22 21 eleq2d ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ↔ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) )
23 20 22 anbi12d ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) ↔ ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) ) )
24 16 adantr ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → 𝑃 = 𝑝 )
25 18 oveqdr ⊢ ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → ( 𝑢 𝐼 𝑦 ) = ( 𝑢 𝑖 𝑦 ) )
26 25 eleq2d ⊢ ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ↔ 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ) )
27 18 oveqdr ⊢ ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → ( 𝑣 𝐼 𝑥 ) = ( 𝑣 𝑖 𝑥 ) )
28 27 eleq2d ⊢ ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → ( 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ↔ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) )
29 26 28 anbi12d ⊢ ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → ( ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ↔ ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) )
30 24 29 rexeqbidva ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ↔ ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) )
31 23 30 imbi12d ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ↔ ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ) )
32 16 31 raleqbidva ⊢ ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) → ( ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ↔ ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ) )
33 15 32 raleqbidva ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ↔ ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ) )
34 14 33 raleqbidva ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ↔ ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ) )
35 6 34 raleqbidva ⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) → ( ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ↔ ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ) )
36 5 35 raleqbidva ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ) )
37 5 pweqd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → 𝒫 𝑃 = 𝒫 𝑝 )
38 37 adantr ⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) → 𝒫 𝑃 = 𝒫 𝑝 )
39 5 ad2antrr ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) → 𝑃 = 𝑝 )
40 simp-4r ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → 𝑖 = 𝐼 )
41 40 eqcomd ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → 𝐼 = 𝑖 )
42 41 oveqd ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → ( 𝑎 𝐼 𝑦 ) = ( 𝑎 𝑖 𝑦 ) )
43 42 eleq2d ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → ( 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) ) )
44 43 2ralbidv ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) ) )
45 39 44 rexeqbidva ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) → ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) ) )
46 simp-4r ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → 𝑖 = 𝐼 )
47 46 eqcomd ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → 𝐼 = 𝑖 )
48 47 oveqd ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( 𝑥 𝐼 𝑦 ) = ( 𝑥 𝑖 𝑦 ) )
49 48 eleq2d ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) )
50 49 2ralbidv ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) )
51 39 50 rexeqbidva ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) → ( ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ↔ ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) )
52 45 51 imbi12d ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑡 ∈ 𝒫 𝑃 ) → ( ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ↔ ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) → ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) ) )
53 38 52 raleqbidva ⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑠 ∈ 𝒫 𝑃 ) → ( ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝑝 ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) → ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) ) )
54 37 53 raleqbidva ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝑝 ∀ 𝑡 ∈ 𝒫 𝑝 ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) → ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) ) )
55 13 36 54 3anbi123d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑝 ∀ 𝑡 ∈ 𝒫 𝑝 ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) → ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) ) ) )
56 1 3 55 sbcie2s ⊢ ( 𝑓 = 𝐺 → ( [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑝 ∀ 𝑡 ∈ 𝒫 𝑝 ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) → ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ) )
57 df-trkgb ⊢ TarskiGB = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑝 ∀ 𝑡 ∈ 𝒫 𝑝 ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) → ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) ) }
58 56 57 elab4g ⊢ ( 𝐺 ∈ TarskiGB ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ) )