f1otrge - Metamath Proof Explorer

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

Theorem f1otrge 27137

Description: A bijection between bases which conserves distances and intervals conserves also the property of being a Euclidean geometry. (Contributed by Thierry Arnoux, 23-Mar-2019.)

**Hypotheses**
Ref	Expression
f1otrkg.p	⊢ 𝑃 = (Base‘𝐺)
f1otrkg.d	⊢ 𝐷 = (dist‘𝐺)
f1otrkg.i	⊢ 𝐼 = (Itv‘𝐺)
f1otrkg.b	⊢ 𝐵 = (Base‘𝐻)
f1otrkg.e	⊢ 𝐸 = (dist‘𝐻)
f1otrkg.j	⊢ 𝐽 = (Itv‘𝐻)
f1otrkg.f	⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)
f1otrkg.1	⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
f1otrkg.2	⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
f1otrg.h	⊢ (𝜑 → 𝐻 ∈ 𝑉)
f1otrge.g	⊢ (𝜑 → 𝐺 ∈ TarskiG_E)

**Assertion**
Ref	Expression
f1otrge	⊢ (𝜑 → 𝐻 ∈ TarskiG_E)

Distinct variable groups: 𝑒,𝑓,𝑔,𝐵 𝐷,𝑒,𝑓,𝑔 𝑒,𝐸,𝑓,𝑔 𝑒,𝐹,𝑓,𝑔 𝑒,𝐼,𝑓,𝑔 𝑒,𝐽,𝑓,𝑔 𝑃,𝑒,𝑓,𝑔 𝜑,𝑒,𝑓,𝑔 𝑓,𝐻 Allowed substitution hints: 𝐺(𝑒,𝑓,𝑔) 𝐻(𝑒,𝑔) 𝑉(𝑒,𝑓,𝑔)

Proof of Theorem f1otrge Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑢 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1otrg.h	. . 3 ⊢ (𝜑 → 𝐻 ∈ 𝑉)
2	1	elexd 3442	. 2 ⊢ (𝜑 → 𝐻 ∈ V)
3		f1otrkg.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)
4		f1ocnv 6712	. . . . . . . . . 10 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → ^◡𝐹:𝑃–1-1-onto→𝐵)
5		f1of 6700	. . . . . . . . . 10 ⊢ (^◡𝐹:𝑃–1-1-onto→𝐵 → ^◡𝐹:𝑃⟶𝐵)
6	3, 4, 5	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ^◡𝐹:𝑃⟶𝐵)
7	6	ad6antr 732	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ^◡𝐹:𝑃⟶𝐵)
8		simpllr 772	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑐 ∈ 𝑃)
9	7, 8	ffvelrnd 6944	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (^◡𝐹‘𝑐) ∈ 𝐵)
10		simplr 765	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑑 ∈ 𝑃)
11	7, 10	ffvelrnd 6944	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (^◡𝐹‘𝑑) ∈ 𝐵)
12		simpr1 1192	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐))
13	3	ad3antrrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐹:𝐵–1-1-onto→𝑃)
14	13	ad3antrrr 726	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝐹:𝐵–1-1-onto→𝑃)
15		f1ocnvfv2 7130	. . . . . . . . . . 11 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → (𝐹‘(^◡𝐹‘𝑐)) = 𝑐)
16	14, 8, 15	syl2anc 583	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘(^◡𝐹‘𝑐)) = 𝑐)
17	16	oveq2d 7271	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑐))) = ((𝐹‘𝑥)𝐼𝑐))
18	12, 17	eleqtrrd 2842	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑐))))
19		f1otrkg.p	. . . . . . . . 9 ⊢ 𝑃 = (Base‘𝐺)
20		f1otrkg.d	. . . . . . . . 9 ⊢ 𝐷 = (dist‘𝐺)
21		f1otrkg.i	. . . . . . . . 9 ⊢ 𝐼 = (Itv‘𝐺)
22		f1otrkg.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐻)
23		f1otrkg.e	. . . . . . . . 9 ⊢ 𝐸 = (dist‘𝐻)
24		f1otrkg.j	. . . . . . . . 9 ⊢ 𝐽 = (Itv‘𝐻)
25		f1otrkg.1	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
26	25	ad5ant15 755	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
27	26	ad5ant15 755	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
28		f1otrkg.2	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
29	28	ad5ant15 755	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
30	29	ad5ant15 755	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
31		simprl 767	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵)
32	31	ad2antrr 722	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑥 ∈ 𝐵)
33	32	ad3antrrr 726	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑥 ∈ 𝐵)
34		simprr 769	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵)
35	34	ad2antrr 722	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑦 ∈ 𝐵)
36	35	ad3antrrr 726	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑦 ∈ 𝐵)
37	19, 20, 21, 22, 23, 24, 14, 27, 30, 33, 9, 36	f1otrgitv 27135	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑐)))))
38	18, 37	mpbird 256	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)))
39		simpr2 1193	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑))
40		f1ocnvfv2 7130	. . . . . . . . . . 11 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑑 ∈ 𝑃) → (𝐹‘(^◡𝐹‘𝑑)) = 𝑑)
41	14, 10, 40	syl2anc 583	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘(^◡𝐹‘𝑑)) = 𝑑)
42	41	oveq2d 7271	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑑))) = ((𝐹‘𝑥)𝐼𝑑))
43	39, 42	eleqtrrd 2842	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑑))))
44		simplr1 1213	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑧 ∈ 𝐵)
45	44	ad3antrrr 726	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑧 ∈ 𝐵)
46	19, 20, 21, 22, 23, 24, 14, 27, 30, 33, 11, 45	f1otrgitv 27135	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)) ↔ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑑)))))
47	43, 46	mpbird 256	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)))
48		simpr3 1194	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))
49	16, 41	oveq12d 7273	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘(^◡𝐹‘𝑐))𝐼(𝐹‘(^◡𝐹‘𝑑))) = (𝑐𝐼𝑑))
50	48, 49	eleqtrrd 2842	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑣) ∈ ((𝐹‘(^◡𝐹‘𝑐))𝐼(𝐹‘(^◡𝐹‘𝑑))))
51		simplr3 1215	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑣 ∈ 𝐵)
52	51	ad3antrrr 726	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑣 ∈ 𝐵)
53	19, 20, 21, 22, 23, 24, 14, 27, 30, 9, 11, 52	f1otrgitv 27135	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)) ↔ (𝐹‘𝑣) ∈ ((𝐹‘(^◡𝐹‘𝑐))𝐼(𝐹‘(^◡𝐹‘𝑑)))))
54	50, 53	mpbird 256	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))
55		oveq2 7263	. . . . . . . . . 10 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑥𝐽𝑎) = (𝑥𝐽(^◡𝐹‘𝑐)))
56	55	eleq2d 2824	. . . . . . . . 9 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑦 ∈ (𝑥𝐽𝑎) ↔ 𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐))))
57		oveq1 7262	. . . . . . . . . 10 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑎𝐽𝑏) = ((^◡𝐹‘𝑐)𝐽𝑏))
58	57	eleq2d 2824	. . . . . . . . 9 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑣 ∈ (𝑎𝐽𝑏) ↔ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏)))
59	56, 58	3anbi13d 1436	. . . . . . . 8 ⊢ (𝑎 = (^◡𝐹‘𝑐) → ((𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏))))
60		oveq2 7263	. . . . . . . . . 10 ⊢ (𝑏 = (^◡𝐹‘𝑑) → (𝑥𝐽𝑏) = (𝑥𝐽(^◡𝐹‘𝑑)))
61	60	eleq2d 2824	. . . . . . . . 9 ⊢ (𝑏 = (^◡𝐹‘𝑑) → (𝑧 ∈ (𝑥𝐽𝑏) ↔ 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑))))
62		oveq2 7263	. . . . . . . . . 10 ⊢ (𝑏 = (^◡𝐹‘𝑑) → ((^◡𝐹‘𝑐)𝐽𝑏) = ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))
63	62	eleq2d 2824	. . . . . . . . 9 ⊢ (𝑏 = (^◡𝐹‘𝑑) → (𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏) ↔ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑))))
64	61, 63	3anbi23d 1437	. . . . . . . 8 ⊢ (𝑏 = (^◡𝐹‘𝑑) → ((𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))))
65	59, 64	rspc2ev 3564	. . . . . . 7 ⊢ (((^◡𝐹‘𝑐) ∈ 𝐵 ∧ (^◡𝐹‘𝑑) ∈ 𝐵 ∧ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))
66	9, 11, 38, 47, 54, 65	syl113anc 1380	. . . . . 6 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))
67		f1otrge.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ TarskiG_E)
68	67	ad3antrrr 726	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐺 ∈ TarskiG_E)
69		f1of 6700	. . . . . . . . . . 11 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵⟶𝑃)
70	3, 69	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵⟶𝑃)
71	70	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹:𝐵⟶𝑃)
72	71, 31	ffvelrnd 6944	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑥) ∈ 𝑃)
73	72	ad2antrr 722	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑥) ∈ 𝑃)
74	71, 34	ffvelrnd 6944	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑦) ∈ 𝑃)
75	74	ad2antrr 722	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑦) ∈ 𝑃)
76	70	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐹:𝐵⟶𝑃)
77	76, 44	ffvelrnd 6944	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑧) ∈ 𝑃)
78		simplr2 1214	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ 𝐵)
79	76, 78	ffvelrnd 6944	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ 𝑃)
80	76, 51	ffvelrnd 6944	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑣) ∈ 𝑃)
81		simpr1 1192	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ (𝑥𝐽𝑣))
82	19, 20, 21, 22, 23, 24, 13, 26, 29, 32, 51, 78	f1otrgitv 27135	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝑢 ∈ (𝑥𝐽𝑣) ↔ (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑣))))
83	81, 82	mpbid 231	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑣)))
84		simpr2 1193	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ (𝑦𝐽𝑧))
85	19, 20, 21, 22, 23, 24, 13, 26, 29, 35, 44, 78	f1otrgitv 27135	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝑢 ∈ (𝑦𝐽𝑧) ↔ (𝐹‘𝑢) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧))))
86	84, 85	mpbid 231	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧)))
87		simpr3 1194	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑥 ≠ 𝑢)
88		dff1o6 7128	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵–1-1-onto→𝑃 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀𝑥 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢)))
89	88	simp3bi 1145	. . . . . . . . . . . 12 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → ∀𝑥 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢))
90	89	r19.21bi 3132	. . . . . . . . . . 11 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) → ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢))
91	90	r19.21bi 3132	. . . . . . . . . 10 ⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢))
92	91	necon3d 2963	. . . . . . . . 9 ⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → (𝑥 ≠ 𝑢 → (𝐹‘𝑥) ≠ (𝐹‘𝑢)))
93	92	imp 406	. . . . . . . 8 ⊢ ((((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ≠ 𝑢) → (𝐹‘𝑥) ≠ (𝐹‘𝑢))
94	13, 32, 78, 87, 93	syl1111anc 836	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑥) ≠ (𝐹‘𝑢))
95	19, 20, 21, 68, 73, 75, 77, 79, 80, 83, 86, 94	axtgeucl 26737	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑)))
96	66, 95	r19.29vva 3263	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))
97	96	ex 412	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))))
98	97	ralrimivvva 3115	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))))
99	98	ralrimivva 3114	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))))
100	22, 23, 24	istrkge 26722	. 2 ⊢ (𝐻 ∈ TarskiG_E ↔ (𝐻 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))))
101	2, 99, 100	sylanbrc 582	1 ⊢ (𝜑 → 𝐻 ∈ TarskiG_E)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 Vcvv 3422 ^◡ccnv 5579 ran crn 5581 Fn wfn 6413 ⟶wf 6414 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 Basecbs 16840 distcds 16897 TarskiG_Ecstrkge 26698 Itvcitv 26699

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pr 5347

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-ov 7258 df-trkge 26716

This theorem is referenced by: (None)

W3C validator