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 29449

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 3474	. 2 ⊢ (𝜑 → 𝐻 ∈ V)
3		f1otrkg.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)
4		f1ocnv 6837	. . . . . . . . . 10 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → ^◡𝐹:𝑃–1-1-onto→𝐵)
5		f1of 6824	. . . . . . . . . 10 ⊢ (^◡𝐹:𝑃–1-1-onto→𝐵 → ^◡𝐹:𝑃⟶𝐵)
6	3, 4, 5	3syl 19	. . . . . . . . 9 ⊢ (𝜑 → ^◡𝐹:𝑃⟶𝐵)
7	6	ad6antr 749	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ^◡𝐹:𝑃⟶𝐵)
8		simpllr 788	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑐 ∈ 𝑃)
9	7, 8	ffvelcdmd 7085	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (^◡𝐹‘𝑐) ∈ 𝐵)
10		simplr 781	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑑 ∈ 𝑃)
11	7, 10	ffvelcdmd 7085	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (^◡𝐹‘𝑑) ∈ 𝐵)
12		simpr1 1213	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐))
13	3	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐹:𝐵–1-1-onto→𝑃)
14	13	ad3antrrr 743	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝐹:𝐵–1-1-onto→𝑃)
15		f1ocnvfv2 7285	. . . . . . . . . . 11 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → (𝐹‘(^◡𝐹‘𝑐)) = 𝑐)
16	14, 8, 15	syl2anc 596	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘(^◡𝐹‘𝑐)) = 𝑐)
17	16	oveq2d 7436	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑐))) = ((𝐹‘𝑥)𝐼𝑐))
18	12, 17	eleqtrrd 2864	. . . . . . . 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 771	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
27	26	ad5ant15 771	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
28		f1otrkg.2	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
29	28	ad5ant15 771	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
30	29	ad5ant15 771	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
31		simprl 783	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵)
32	31	ad2antrr 739	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑥 ∈ 𝐵)
33	32	ad3antrrr 743	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑥 ∈ 𝐵)
34		simprr 785	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵)
35	34	ad2antrr 739	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑦 ∈ 𝐵)
36	35	ad3antrrr 743	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑦 ∈ 𝐵)
37	19, 20, 21, 22, 23, 24, 14, 27, 30, 33, 9, 36	f1otrgitv 29447	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑐)))))
38	18, 37	mpbird 260	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)))
39		simpr2 1214	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑))
40		f1ocnvfv2 7285	. . . . . . . . . . 11 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑑 ∈ 𝑃) → (𝐹‘(^◡𝐹‘𝑑)) = 𝑑)
41	14, 10, 40	syl2anc 596	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘(^◡𝐹‘𝑑)) = 𝑑)
42	41	oveq2d 7436	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑑))) = ((𝐹‘𝑥)𝐼𝑑))
43	39, 42	eleqtrrd 2864	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑑))))
44		simplr1 1234	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑧 ∈ 𝐵)
45	44	ad3antrrr 743	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑧 ∈ 𝐵)
46	19, 20, 21, 22, 23, 24, 14, 27, 30, 33, 11, 45	f1otrgitv 29447	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)) ↔ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑑)))))
47	43, 46	mpbird 260	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)))
48		simpr3 1215	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))
49	16, 41	oveq12d 7438	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘(^◡𝐹‘𝑐))𝐼(𝐹‘(^◡𝐹‘𝑑))) = (𝑐𝐼𝑑))
50	48, 49	eleqtrrd 2864	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑣) ∈ ((𝐹‘(^◡𝐹‘𝑐))𝐼(𝐹‘(^◡𝐹‘𝑑))))
51		simplr3 1236	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑣 ∈ 𝐵)
52	51	ad3antrrr 743	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑣 ∈ 𝐵)
53	19, 20, 21, 22, 23, 24, 14, 27, 30, 9, 11, 52	f1otrgitv 29447	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)) ↔ (𝐹‘𝑣) ∈ ((𝐹‘(^◡𝐹‘𝑐))𝐼(𝐹‘(^◡𝐹‘𝑑)))))
54	50, 53	mpbird 260	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))
55		oveq2 7428	. . . . . . . . . 10 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑥𝐽𝑎) = (𝑥𝐽(^◡𝐹‘𝑐)))
56	55	eleq2d 2847	. . . . . . . . 9 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑦 ∈ (𝑥𝐽𝑎) ↔ 𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐))))
57		oveq1 7427	. . . . . . . . . 10 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑎𝐽𝑏) = ((^◡𝐹‘𝑐)𝐽𝑏))
58	57	eleq2d 2847	. . . . . . . . 9 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑣 ∈ (𝑎𝐽𝑏) ↔ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏)))
59	56, 58	3anbi13d 1466	. . . . . . . 8 ⊢ (𝑎 = (^◡𝐹‘𝑐) → ((𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏))))
60		oveq2 7428	. . . . . . . . . 10 ⊢ (𝑏 = (^◡𝐹‘𝑑) → (𝑥𝐽𝑏) = (𝑥𝐽(^◡𝐹‘𝑑)))
61	60	eleq2d 2847	. . . . . . . . 9 ⊢ (𝑏 = (^◡𝐹‘𝑑) → (𝑧 ∈ (𝑥𝐽𝑏) ↔ 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑))))
62		oveq2 7428	. . . . . . . . . 10 ⊢ (𝑏 = (^◡𝐹‘𝑑) → ((^◡𝐹‘𝑐)𝐽𝑏) = ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))
63	62	eleq2d 2847	. . . . . . . . 9 ⊢ (𝑏 = (^◡𝐹‘𝑑) → (𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏) ↔ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑))))
64	61, 63	3anbi23d 1467	. . . . . . . 8 ⊢ (𝑏 = (^◡𝐹‘𝑑) → ((𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))))
65	59, 64	rspc2ev 3589	. . . . . . 7 ⊢ (((^◡𝐹‘𝑐) ∈ 𝐵 ∧ (^◡𝐹‘𝑑) ∈ 𝐵 ∧ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))
66	9, 11, 38, 47, 54, 65	syl113anc 1409	. . . . . 6 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))
67		f1otrge.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ TarskiG_E)
68	67	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐺 ∈ TarskiG_E)
69		f1of 6824	. . . . . . . . . . 11 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵⟶𝑃)
70	3, 69	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵⟶𝑃)
71	70	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹:𝐵⟶𝑃)
72	71, 31	ffvelcdmd 7085	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑥) ∈ 𝑃)
73	72	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑥) ∈ 𝑃)
74	71, 34	ffvelcdmd 7085	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑦) ∈ 𝑃)
75	74	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑦) ∈ 𝑃)
76	70	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐹:𝐵⟶𝑃)
77	76, 44	ffvelcdmd 7085	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑧) ∈ 𝑃)
78		simplr2 1235	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ 𝐵)
79	76, 78	ffvelcdmd 7085	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ 𝑃)
80	76, 51	ffvelcdmd 7085	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑣) ∈ 𝑃)
81		simpr1 1213	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ (𝑥𝐽𝑣))
82	19, 20, 21, 22, 23, 24, 13, 26, 29, 32, 51, 78	f1otrgitv 29447	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝑢 ∈ (𝑥𝐽𝑣) ↔ (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑣))))
83	81, 82	mpbid 235	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑣)))
84		simpr2 1214	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ (𝑦𝐽𝑧))
85	19, 20, 21, 22, 23, 24, 13, 26, 29, 35, 44, 78	f1otrgitv 29447	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝑢 ∈ (𝑦𝐽𝑧) ↔ (𝐹‘𝑢) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧))))
86	84, 85	mpbid 235	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧)))
87		simpr3 1215	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑥 ≠ 𝑢)
88		dff1o6 7283	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵–1-1-onto→𝑃 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀𝑥 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢)))
89	88	simp3bi 1165	. . . . . . . . . . . 12 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → ∀𝑥 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢))
90	89	r19.21bi 3255	. . . . . . . . . . 11 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) → ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢))
91	90	r19.21bi 3255	. . . . . . . . . 10 ⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢))
92	91	necon3d 2977	. . . . . . . . 9 ⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → (𝑥 ≠ 𝑢 → (𝐹‘𝑥) ≠ (𝐹‘𝑢)))
93	92	imp 412	. . . . . . . 8 ⊢ ((((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ≠ 𝑢) → (𝐹‘𝑥) ≠ (𝐹‘𝑢))
94	13, 32, 78, 87, 93	syl1111anc 854	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑥) ≠ (𝐹‘𝑢))
95	19, 20, 21, 68, 73, 75, 77, 79, 80, 83, 86, 94	axtgeucl 28934	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑)))
96	66, 95	r19.29vva 3223	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))
97	96	ex 418	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))))
98	97	ralrimivvva 3209	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))))
99	98	ralrimivva 3206	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))))
100	22, 23, 24	istrkge 28919	. 2 ⊢ (𝐻 ∈ TarskiG_E ↔ (𝐻 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))))
101	2, 99, 100	sylanbrc 595	1 ⊢ (𝜑 → 𝐻 ∈ TarskiG_E)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 Vcvv 3451 ^◡ccnv 5650 ran crn 5652 Fn wfn 6533 ⟶wf 6534 –1-1-onto→wf1o 6537 ‘cfv 6538 (class class class)co 7420 Basecbs 17387 distcds 17437 TarskiG_Ecstrkge 28894 Itvcitv 28895

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pr 5391

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-ne 2957 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-sbc 3740 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-ov 7423 df-trkge 28913

This theorem is used by: (None)

W3C validator