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	⊢ ( 𝐺 ∈ TarskiG_B ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		istrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		istrkg.d	⊢ − = ( dist ‘ 𝐺 )
3		istrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		simpl	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → 𝑝 = 𝑃 )
5		simpr	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → 𝑖 = 𝐼 )
6	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑥 𝑖 𝑥 ) = ( 𝑥 𝐼 𝑥 ) )
7	6	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) ↔ 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) ) )
8	7	imbi1d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) → 𝑥 = 𝑦 ) ↔ ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ) )
9	4 8	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑦 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ) )
10	4 9	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ) )
11	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑥 𝑖 𝑧 ) = ( 𝑥 𝐼 𝑧 ) )
12	11	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ↔ 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ) )
13	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑦 𝑖 𝑧 ) = ( 𝑦 𝐼 𝑧 ) )
14	13	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ↔ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) )
15	12 14	anbi12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) ↔ ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) ) )
16	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑢 𝑖 𝑦 ) = ( 𝑢 𝐼 𝑦 ) )
17	16	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ↔ 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ) )
18	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑣 𝑖 𝑥 ) = ( 𝑣 𝐼 𝑥 ) )
19	18	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ↔ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) )
20	17 19	anbi12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ↔ ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) )
21	4 20	rexeqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) )
22	15 21	imbi12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ↔ ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ) )
23	4 22	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ↔ ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ) )
24	4 23	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ) )
25	4 24	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ↔ ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ) )
26	4 25	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ↔ ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ) )
27	4 26	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ) )
28	4	pweqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → 𝒫 𝑝 = 𝒫 𝑃 )
29	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑎 𝑖 𝑦 ) = ( 𝑎 𝐼 𝑦 ) )
30	29	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) ↔ 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ) )
31	30	2ralbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ) )
32	4 31	rexeqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) ↔ ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ) )
33	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑥 𝑖 𝑦 ) = ( 𝑥 𝐼 𝑦 ) )
34	33	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ↔ 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
35	34	2ralbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
36	4 35	rexeqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ↔ ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
37	32 36	imbi12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) → ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) ↔ ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
38	28 37	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑡 ∈ 𝒫 𝑝 ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) → ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
39	28 38	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑠 ∈ 𝒫 𝑝 ∀ 𝑡 ∈ 𝒫 𝑝 ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) → ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
40	10 27 39	3anbi123d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑝 ∀ 𝑡 ∈ 𝒫 𝑝 ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) → ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ) )
41	1 3 40	sbcie2s	⊢ ( 𝑓 = 𝐺 → ( [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑝 ∀ 𝑡 ∈ 𝒫 𝑝 ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) → ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ) )
42		df-trkgb	⊢ TarskiG_B = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝑖 𝑧 ) ) → ∃ 𝑎 ∈ 𝑝 ( 𝑎 ∈ ( 𝑢 𝑖 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝑖 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑝 ∀ 𝑡 ∈ 𝒫 𝑝 ( ∃ 𝑎 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝑖 𝑦 ) → ∃ 𝑏 ∈ 𝑝 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝑖 𝑦 ) ) ) }
43	41 42	elab4g	⊢ ( 𝐺 ∈ TarskiG_B ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ) )

Metamath Proof Explorer

Theorem istrkgb

Proof