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 28353

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 28338	. . . . . 6 ⊢ (𝐺 ∈ TarskiG_E ↔ (𝐺 ∈ V ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
9	4, 8	sylib 217	. . . . 5 ⊢ (𝜑 → (𝐺 ∈ V ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
10	9	simprd 494	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
11		axtgeucl.1	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
12		axtgeucl.2	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
13		axtgeucl.3	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
14		oveq1 7426	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑣) = (𝑋𝐼𝑣))
15	14	eleq2d 2811	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑢 ∈ (𝑥𝐼𝑣) ↔ 𝑢 ∈ (𝑋𝐼𝑣)))
16		neeq1 2992	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑥 ≠ 𝑢 ↔ 𝑋 ≠ 𝑢))
17	15, 16	3anbi13d 1434	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) ↔ (𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢)))
18		oveq1 7426	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑎) = (𝑋𝐼𝑎))
19	18	eleq2d 2811	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑎) ↔ 𝑦 ∈ (𝑋𝐼𝑎)))
20		oveq1 7426	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑏) = (𝑋𝐼𝑏))
21	20	eleq2d 2811	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (𝑧 ∈ (𝑥𝐼𝑏) ↔ 𝑧 ∈ (𝑋𝐼𝑏)))
22	19, 21	3anbi12d 1433	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ((𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
23	22	2rexbidv 3209	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
24	17, 23	imbi12d 343	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
25	24	2ralbidv 3208	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
26		oveq1 7426	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (𝑦𝐼𝑧) = (𝑌𝐼𝑧))
27	26	eleq2d 2811	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → (𝑢 ∈ (𝑦𝐼𝑧) ↔ 𝑢 ∈ (𝑌𝐼𝑧)))
28	27	3anbi2d 1437	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) ↔ (𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢)))
29		eleq1 2813	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑎) ↔ 𝑌 ∈ (𝑋𝐼𝑎)))
30	29	3anbi1d 1436	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → ((𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
31	30	2rexbidv 3209	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
32	28, 31	imbi12d 343	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
33	32	2ralbidv 3208	. . . . . 6 ⊢ (𝑦 = 𝑌 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
34		oveq2 7427	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (𝑌𝐼𝑧) = (𝑌𝐼𝑍))
35	34	eleq2d 2811	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → (𝑢 ∈ (𝑌𝐼𝑧) ↔ 𝑢 ∈ (𝑌𝐼𝑍)))
36	35	3anbi2d 1437	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) ↔ (𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢)))
37		eleq1 2813	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (𝑧 ∈ (𝑋𝐼𝑏) ↔ 𝑍 ∈ (𝑋𝐼𝑏)))
38	37	3anbi2d 1437	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → ((𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
39	38	2rexbidv 3209	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
40	36, 39	imbi12d 343	. . . . . . 7 ⊢ (𝑧 = 𝑍 → (((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
41	40	2ralbidv 3208	. . . . . 6 ⊢ (𝑧 = 𝑍 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
42	25, 33, 41	rspc3v 3622	. . . . 5 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
43	11, 12, 13, 42	syl3anc 1368	. . . 4 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
44	10, 43	mpd 15	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))
45		axtgeucl.4	. . . 4 ⊢ (𝜑 → 𝑈 ∈ 𝑃)
46		axtgeucl.5	. . . 4 ⊢ (𝜑 → 𝑉 ∈ 𝑃)
47		eleq1 2813	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (𝑢 ∈ (𝑋𝐼𝑣) ↔ 𝑈 ∈ (𝑋𝐼𝑣)))
48		eleq1 2813	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (𝑢 ∈ (𝑌𝐼𝑍) ↔ 𝑈 ∈ (𝑌𝐼𝑍)))
49		neeq2 2993	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (𝑋 ≠ 𝑢 ↔ 𝑋 ≠ 𝑈))
50	47, 48, 49	3anbi123d 1432	. . . . . 6 ⊢ (𝑢 = 𝑈 → ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) ↔ (𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈)))
51	50	imbi1d 340	. . . . 5 ⊢ (𝑢 = 𝑈 → (((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))))
52		oveq2 7427	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → (𝑋𝐼𝑣) = (𝑋𝐼𝑉))
53	52	eleq2d 2811	. . . . . . 7 ⊢ (𝑣 = 𝑉 → (𝑈 ∈ (𝑋𝐼𝑣) ↔ 𝑈 ∈ (𝑋𝐼𝑉)))
54	53	3anbi1d 1436	. . . . . 6 ⊢ (𝑣 = 𝑉 → ((𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) ↔ (𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈)))
55		eleq1 2813	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → (𝑣 ∈ (𝑎𝐼𝑏) ↔ 𝑉 ∈ (𝑎𝐼𝑏)))
56	55	3anbi3d 1438	. . . . . . 7 ⊢ (𝑣 = 𝑉 → ((𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))))
57	56	2rexbidv 3209	. . . . . 6 ⊢ (𝑣 = 𝑉 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))))
58	54, 57	imbi12d 343	. . . . 5 ⊢ (𝑣 = 𝑉 → (((𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))))
59	51, 58	rspc2v 3617	. . . 4 ⊢ ((𝑈 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃) → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))))
60	45, 46, 59	syl2anc 582	. . 3 ⊢ (𝜑 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))))
61	44, 60	mpd 15	. 2 ⊢ (𝜑 → ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))))
62	1, 2, 3, 61	mp3and 1460	1 ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ≠ wne 2929 ∀wral 3050 ∃wrex 3059 Vcvv 3461 ‘cfv 6549 (class class class)co 7419 Basecbs 17188 distcds 17250 TarskiG_Ecstrkge 28313 Itvcitv 28314

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-nul 5307

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ne 2930 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-sbc 3774 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-iota 6501 df-fv 6557 df-ov 7422 df-trkge 28332

This theorem is referenced by: f1otrge 28753

W3C validator