Theorem axtgcont1

Description: Axiom of Continuity. Axiom A11 of Schwabhauser p. 13. This axiom (scheme) asserts that any two sets S and T (of points) such that the elements of S precede the elements of T with respect to some point a (that is, x is between a and y whenever x is in X and y is in Y ) are separated by some point b ; this is explained in Axiom 11 of Tarski1999 p. 185. (Contributed by Thierry Arnoux, 16-Mar-2019)

	Ref	Expression
Hypotheses	axtrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	axtrkg.d	⊢ − = ( dist ‘ 𝐺 )
	axtrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	axtrkg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	axtgcont.1	⊢ ( 𝜑 → 𝑆 ⊆ 𝑃 )
	axtgcont.2	⊢ ( 𝜑 → 𝑇 ⊆ 𝑃 )
Assertion	axtgcont1	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		axtrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		axtrkg.d	⊢ − = ( dist ‘ 𝐺 )
3		axtrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		axtrkg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		axtgcont.1	⊢ ( 𝜑 → 𝑆 ⊆ 𝑃 )
6		axtgcont.2	⊢ ( 𝜑 → 𝑇 ⊆ 𝑃 )
7		df-trkg	⊢ TarskiG = ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) )
8		inss1	⊢ ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) ) ⊆ ( TarskiGC ∩ TarskiGB )
9		inss2	⊢ ( TarskiGC ∩ TarskiGB ) ⊆ TarskiGB
10	8 9	sstri	⊢ ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) ) ⊆ TarskiGB
11	7 10	eqsstri	⊢ TarskiG ⊆ TarskiGB
12	11 4	sselid	⊢ ( 𝜑 → 𝐺 ∈ TarskiGB )
13	1 2 3	istrkgb	⊢ ( 𝐺 ∈ TarskiGB ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ) )
14	13	simprbi	⊢ ( 𝐺 ∈ TarskiGB → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
15	14	simp3d	⊢ ( 𝐺 ∈ TarskiGB → ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
16	12 15	syl	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
17	1	fvexi	⊢ 𝑃 ∈ V
18	17	ssex	⊢ ( 𝑆 ⊆ 𝑃 → 𝑆 ∈ V )
19		elpwg	⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ 𝒫 𝑃 ↔ 𝑆 ⊆ 𝑃 ) )
20	5 18 19	3syl	⊢ ( 𝜑 → ( 𝑆 ∈ 𝒫 𝑃 ↔ 𝑆 ⊆ 𝑃 ) )
21	5 20	mpbird	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝑃 )
22	17	ssex	⊢ ( 𝑇 ⊆ 𝑃 → 𝑇 ∈ V )
23		elpwg	⊢ ( 𝑇 ∈ V → ( 𝑇 ∈ 𝒫 𝑃 ↔ 𝑇 ⊆ 𝑃 ) )
24	6 22 23	3syl	⊢ ( 𝜑 → ( 𝑇 ∈ 𝒫 𝑃 ↔ 𝑇 ⊆ 𝑃 ) )
25	6 24	mpbird	⊢ ( 𝜑 → 𝑇 ∈ 𝒫 𝑃 )
26		raleq	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ) )
27	26	rexbidv	⊢ ( 𝑠 = 𝑆 → ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ) )
28		raleq	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
29	28	rexbidv	⊢ ( 𝑠 = 𝑆 → ( ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ↔ ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
30	27 29	imbi12d	⊢ ( 𝑠 = 𝑆 → ( ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ↔ ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
31		raleq	⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ) )
32	31	rexralbidv	⊢ ( 𝑡 = 𝑇 → ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ) )
33		raleq	⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
34	33	rexralbidv	⊢ ( 𝑡 = 𝑇 → ( ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ↔ ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
35	32 34	imbi12d	⊢ ( 𝑡 = 𝑇 → ( ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ↔ ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
36	30 35	rspc2v	⊢ ( ( 𝑆 ∈ 𝒫 𝑃 ∧ 𝑇 ∈ 𝒫 𝑃 ) → ( ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) → ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
37	21 25 36	syl2anc	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) → ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
38	16 37	mpd	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )