axtgeucl - Metamath Proof Explorer

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

Theorem axtgeucl 25371

Description: Euclid's Axiom. Axiom A10 of [Schwabhauser] p. 13. This is equivalent to Euclid's parallel postulate when combined with other axioms. (Contributed by Thierry Arnoux, 16-Mar-2019.)

**Hypotheses**
Ref	Expression
axtrkge.p	⊢ 𝑃 = (Base‘𝐺)
axtrkge.d	⊢ − = (dist‘𝐺)
axtrkge.i	⊢ 𝐼 = (Itv‘𝐺)
axtgeucl.g	⊢ (𝜑 → 𝐺 ∈ TarskiG_E)
axtgeucl.1	⊢ (𝜑 → 𝑋 ∈ 𝑃)
axtgeucl.2	⊢ (𝜑 → 𝑌 ∈ 𝑃)
axtgeucl.3	⊢ (𝜑 → 𝑍 ∈ 𝑃)
axtgeucl.4	⊢ (𝜑 → 𝑈 ∈ 𝑃)
axtgeucl.5	⊢ (𝜑 → 𝑉 ∈ 𝑃)
axtgeucl.6	⊢ (𝜑 → 𝑈 ∈ (𝑋𝐼𝑉))
axtgeucl.7	⊢ (𝜑 → 𝑈 ∈ (𝑌𝐼𝑍))
axtgeucl.8	⊢ (𝜑 → 𝑋 ≠ 𝑈)

**Assertion**
Ref	Expression
axtgeucl	⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))

Distinct variable groups: 𝑎,𝑏,𝐼 𝑃,𝑎,𝑏 𝑉,𝑎,𝑏 𝑈,𝑎,𝑏 𝑋,𝑎,𝑏 𝑌,𝑎,𝑏 𝑍,𝑎,𝑏 − ,𝑎,𝑏 Allowed substitution hints: 𝜑(𝑎,𝑏) 𝐺(𝑎,𝑏)

Proof of Theorem axtgeucl Dummy variables 𝑣 𝑢 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		axtgeucl.6	. 2 ⊢ (𝜑 → 𝑈 ∈ (𝑋𝐼𝑉))
2		axtgeucl.7	. 2 ⊢ (𝜑 → 𝑈 ∈ (𝑌𝐼𝑍))
3		axtgeucl.8	. 2 ⊢ (𝜑 → 𝑋 ≠ 𝑈)
4		axtgeucl.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG_E)
5		axtrkge.p	. . . . . . 7 ⊢ 𝑃 = (Base‘𝐺)
6		axtrkge.d	. . . . . . 7 ⊢ − = (dist‘𝐺)
7		axtrkge.i	. . . . . . 7 ⊢ 𝐼 = (Itv‘𝐺)
8	5, 6, 7	istrkge 25356	. . . . . 6 ⊢ (𝐺 ∈ TarskiG_E ↔ (𝐺 ∈ V ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
9	4, 8	sylib 208	. . . . 5 ⊢ (𝜑 → (𝐺 ∈ V ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
10	9	simprd 479	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
11		axtgeucl.1	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
12		axtgeucl.2	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
13		axtgeucl.3	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
14		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑣) = (𝑋𝐼𝑣))
15	14	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑢 ∈ (𝑥𝐼𝑣) ↔ 𝑢 ∈ (𝑋𝐼𝑣)))
16		neeq1 2856	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑥 ≠ 𝑢 ↔ 𝑋 ≠ 𝑢))
17	15, 16	3anbi13d 1401	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) ↔ (𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢)))
18		oveq1 6657	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑎) = (𝑋𝐼𝑎))
19	18	eleq2d 2687	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑎) ↔ 𝑦 ∈ (𝑋𝐼𝑎)))
20		oveq1 6657	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑏) = (𝑋𝐼𝑏))
21	20	eleq2d 2687	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (𝑧 ∈ (𝑥𝐼𝑏) ↔ 𝑧 ∈ (𝑋𝐼𝑏)))
22	19, 21	3anbi12d 1400	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ((𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
23	22	2rexbidv 3057	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
24	17, 23	imbi12d 334	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
25	24	2ralbidv 2989	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
26		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (𝑦𝐼𝑧) = (𝑌𝐼𝑧))
27	26	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → (𝑢 ∈ (𝑦𝐼𝑧) ↔ 𝑢 ∈ (𝑌𝐼𝑧)))
28	27	3anbi2d 1404	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) ↔ (𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢)))
29		eleq1 2689	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑎) ↔ 𝑌 ∈ (𝑋𝐼𝑎)))
30	29	3anbi1d 1403	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → ((𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
31	30	2rexbidv 3057	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
32	28, 31	imbi12d 334	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
33	32	2ralbidv 2989	. . . . . 6 ⊢ (𝑦 = 𝑌 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
34		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (𝑌𝐼𝑧) = (𝑌𝐼𝑍))
35	34	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → (𝑢 ∈ (𝑌𝐼𝑧) ↔ 𝑢 ∈ (𝑌𝐼𝑍)))
36	35	3anbi2d 1404	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) ↔ (𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢)))
37		eleq1 2689	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (𝑧 ∈ (𝑋𝐼𝑏) ↔ 𝑍 ∈ (𝑋𝐼𝑏)))
38	37	3anbi2d 1404	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → ((𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
39	38	2rexbidv 3057	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
40	36, 39	imbi12d 334	. . . . . . 7 ⊢ (𝑧 = 𝑍 → (((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
41	40	2ralbidv 2989	. . . . . 6 ⊢ (𝑧 = 𝑍 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
42	25, 33, 41	rspc3v 3325	. . . . 5 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
43	11, 12, 13, 42	syl3anc 1326	. . . 4 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
44	10, 43	mpd 15	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
45		axtgeucl.4	. . . 4 ⊢ (𝜑 → 𝑈 ∈ 𝑃)
46		axtgeucl.5	. . . 4 ⊢ (𝜑 → 𝑉 ∈ 𝑃)
47		eleq1 2689	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (𝑢 ∈ (𝑋𝐼𝑣) ↔ 𝑈 ∈ (𝑋𝐼𝑣)))
48		eleq1 2689	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (𝑢 ∈ (𝑌𝐼𝑍) ↔ 𝑈 ∈ (𝑌𝐼𝑍)))
49		neeq2 2857	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (𝑋 ≠ 𝑢 ↔ 𝑋 ≠ 𝑈))
50	47, 48, 49	3anbi123d 1399	. . . . . 6 ⊢ (𝑢 = 𝑈 → ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) ↔ (𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈)))
51	50	imbi1d 331	. . . . 5 ⊢ (𝑢 = 𝑈 → (((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
52		oveq2 6658	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → (𝑋𝐼𝑣) = (𝑋𝐼𝑉))
53	52	eleq2d 2687	. . . . . . 7 ⊢ (𝑣 = 𝑉 → (𝑈 ∈ (𝑋𝐼𝑣) ↔ 𝑈 ∈ (𝑋𝐼𝑉)))
54	53	3anbi1d 1403	. . . . . 6 ⊢ (𝑣 = 𝑉 → ((𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) ↔ (𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈)))
55		eleq1 2689	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → (𝑣 ∈ (𝑎𝐼𝑏) ↔ 𝑉 ∈ (𝑎𝐼𝑏)))
56	55	3anbi3d 1405	. . . . . . 7 ⊢ (𝑣 = 𝑉 → ((𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))))
57	56	2rexbidv 3057	. . . . . 6 ⊢ (𝑣 = 𝑉 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))))
58	54, 57	imbi12d 334	. . . . 5 ⊢ (𝑣 = 𝑉 → (((𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))))
59	51, 58	rspc2v 3322	. . . 4 ⊢ ((𝑈 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃) → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))))
60	45, 46, 59	syl2anc 693	. . 3 ⊢ (𝜑 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))))
61	44, 60	mpd 15	. 2 ⊢ (𝜑 → ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))))
62	1, 2, 3, 61	mp3and 1427	1 ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 Vcvv 3200 ‘cfv 5888 (class class class)co 6650 Basecbs 15857 distcds 15950 TarskiG_Ecstrkge 25334 Itvcitv 25335

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-nul 4789

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 df-trkge 25350

This theorem is referenced by: f1otrge 25752

W3C validator