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 28495

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 28480	. . . . . 6 ⊢ (𝐺 ∈ TarskiG_E ↔ (𝐺 ∈ V ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
9	4, 8	sylib 218	. . . . 5 ⊢ (𝜑 → (𝐺 ∈ V ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
10	9	simprd 495	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
11		axtgeucl.1	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
12		axtgeucl.2	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
13		axtgeucl.3	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
14		oveq1 7438	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑣) = (𝑋𝐼𝑣))
15	14	eleq2d 2825	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑢 ∈ (𝑥𝐼𝑣) ↔ 𝑢 ∈ (𝑋𝐼𝑣)))
16		neeq1 3001	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑥 ≠ 𝑢 ↔ 𝑋 ≠ 𝑢))
17	15, 16	3anbi13d 1437	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) ↔ (𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢)))
18		oveq1 7438	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑎) = (𝑋𝐼𝑎))
19	18	eleq2d 2825	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑎) ↔ 𝑦 ∈ (𝑋𝐼𝑎)))
20		oveq1 7438	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑏) = (𝑋𝐼𝑏))
21	20	eleq2d 2825	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (𝑧 ∈ (𝑥𝐼𝑏) ↔ 𝑧 ∈ (𝑋𝐼𝑏)))
22	19, 21	3anbi12d 1436	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ((𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
23	22	2rexbidv 3220	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
24	17, 23	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
25	24	2ralbidv 3219	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
26		oveq1 7438	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (𝑦𝐼𝑧) = (𝑌𝐼𝑧))
27	26	eleq2d 2825	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → (𝑢 ∈ (𝑦𝐼𝑧) ↔ 𝑢 ∈ (𝑌𝐼𝑧)))
28	27	3anbi2d 1440	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) ↔ (𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢)))
29		eleq1 2827	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑎) ↔ 𝑌 ∈ (𝑋𝐼𝑎)))
30	29	3anbi1d 1439	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → ((𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
31	30	2rexbidv 3220	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
32	28, 31	imbi12d 344	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
33	32	2ralbidv 3219	. . . . . 6 ⊢ (𝑦 = 𝑌 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
34		oveq2 7439	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (𝑌𝐼𝑧) = (𝑌𝐼𝑍))
35	34	eleq2d 2825	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → (𝑢 ∈ (𝑌𝐼𝑧) ↔ 𝑢 ∈ (𝑌𝐼𝑍)))
36	35	3anbi2d 1440	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) ↔ (𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢)))
37		eleq1 2827	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (𝑧 ∈ (𝑋𝐼𝑏) ↔ 𝑍 ∈ (𝑋𝐼𝑏)))
38	37	3anbi2d 1440	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → ((𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
39	38	2rexbidv 3220	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
40	36, 39	imbi12d 344	. . . . . . 7 ⊢ (𝑧 = 𝑍 → (((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
41	40	2ralbidv 3219	. . . . . 6 ⊢ (𝑧 = 𝑍 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
42	25, 33, 41	rspc3v 3638	. . . . 5 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
43	11, 12, 13, 42	syl3anc 1370	. . . 4 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
44	10, 43	mpd 15	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
45		axtgeucl.4	. . . 4 ⊢ (𝜑 → 𝑈 ∈ 𝑃)
46		axtgeucl.5	. . . 4 ⊢ (𝜑 → 𝑉 ∈ 𝑃)
47		eleq1 2827	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (𝑢 ∈ (𝑋𝐼𝑣) ↔ 𝑈 ∈ (𝑋𝐼𝑣)))
48		eleq1 2827	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (𝑢 ∈ (𝑌𝐼𝑍) ↔ 𝑈 ∈ (𝑌𝐼𝑍)))
49		neeq2 3002	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (𝑋 ≠ 𝑢 ↔ 𝑋 ≠ 𝑈))
50	47, 48, 49	3anbi123d 1435	. . . . . 6 ⊢ (𝑢 = 𝑈 → ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) ↔ (𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈)))
51	50	imbi1d 341	. . . . 5 ⊢ (𝑢 = 𝑈 → (((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
52		oveq2 7439	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → (𝑋𝐼𝑣) = (𝑋𝐼𝑉))
53	52	eleq2d 2825	. . . . . . 7 ⊢ (𝑣 = 𝑉 → (𝑈 ∈ (𝑋𝐼𝑣) ↔ 𝑈 ∈ (𝑋𝐼𝑉)))
54	53	3anbi1d 1439	. . . . . 6 ⊢ (𝑣 = 𝑉 → ((𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) ↔ (𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈)))
55		eleq1 2827	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → (𝑣 ∈ (𝑎𝐼𝑏) ↔ 𝑉 ∈ (𝑎𝐼𝑏)))
56	55	3anbi3d 1441	. . . . . . 7 ⊢ (𝑣 = 𝑉 → ((𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))))
57	56	2rexbidv 3220	. . . . . 6 ⊢ (𝑣 = 𝑉 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))))
58	54, 57	imbi12d 344	. . . . 5 ⊢ (𝑣 = 𝑉 → (((𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))))
59	51, 58	rspc2v 3633	. . . 4 ⊢ ((𝑈 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃) → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))))
60	45, 46, 59	syl2anc 584	. . 3 ⊢ (𝜑 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))))
61	44, 60	mpd 15	. 2 ⊢ (𝜑 → ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))))
62	1, 2, 3, 61	mp3and 1463	1 ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 ∀wral 3059 ∃wrex 3068 Vcvv 3478 ‘cfv 6563 (class class class)co 7431 Basecbs 17245 distcds 17307 TarskiG_Ecstrkge 28455 Itvcitv 28456

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-nul 5312

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3434 df-v 3480 df-sbc 3792 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-br 5149 df-iota 6516 df-fv 6571 df-ov 7434 df-trkge 28474

This theorem is referenced by: f1otrge 28895

W3C validator