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 27814

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 3465	. 2 ⊢ (𝜑 → 𝐻 ∈ V)
3		f1otrkg.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)
4		f1ocnv 6796	. . . . . . . . . 10 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → ^◡𝐹:𝑃–1-1-onto→𝐵)
5		f1of 6784	. . . . . . . . . 10 ⊢ (^◡𝐹:𝑃–1-1-onto→𝐵 → ^◡𝐹:𝑃⟶𝐵)
6	3, 4, 5	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ^◡𝐹:𝑃⟶𝐵)
7	6	ad6antr 734	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ^◡𝐹:𝑃⟶𝐵)
8		simpllr 774	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑐 ∈ 𝑃)
9	7, 8	ffvelcdmd 7036	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (^◡𝐹‘𝑐) ∈ 𝐵)
10		simplr 767	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑑 ∈ 𝑃)
11	7, 10	ffvelcdmd 7036	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (^◡𝐹‘𝑑) ∈ 𝐵)
12		simpr1 1194	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐))
13	3	ad3antrrr 728	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐹:𝐵–1-1-onto→𝑃)
14	13	ad3antrrr 728	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝐹:𝐵–1-1-onto→𝑃)
15		f1ocnvfv2 7223	. . . . . . . . . . 11 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → (𝐹‘(^◡𝐹‘𝑐)) = 𝑐)
16	14, 8, 15	syl2anc 584	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘(^◡𝐹‘𝑐)) = 𝑐)
17	16	oveq2d 7373	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑐))) = ((𝐹‘𝑥)𝐼𝑐))
18	12, 17	eleqtrrd 2841	. . . . . . . 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 757	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
27	26	ad5ant15 757	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
28		f1otrkg.2	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
29	28	ad5ant15 757	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
30	29	ad5ant15 757	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
31		simprl 769	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵)
32	31	ad2antrr 724	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑥 ∈ 𝐵)
33	32	ad3antrrr 728	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑥 ∈ 𝐵)
34		simprr 771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵)
35	34	ad2antrr 724	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑦 ∈ 𝐵)
36	35	ad3antrrr 728	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑦 ∈ 𝐵)
37	19, 20, 21, 22, 23, 24, 14, 27, 30, 33, 9, 36	f1otrgitv 27812	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑐)))))
38	18, 37	mpbird 256	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)))
39		simpr2 1195	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑))
40		f1ocnvfv2 7223	. . . . . . . . . . 11 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑑 ∈ 𝑃) → (𝐹‘(^◡𝐹‘𝑑)) = 𝑑)
41	14, 10, 40	syl2anc 584	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘(^◡𝐹‘𝑑)) = 𝑑)
42	41	oveq2d 7373	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑑))) = ((𝐹‘𝑥)𝐼𝑑))
43	39, 42	eleqtrrd 2841	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑑))))
44		simplr1 1215	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑧 ∈ 𝐵)
45	44	ad3antrrr 728	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑧 ∈ 𝐵)
46	19, 20, 21, 22, 23, 24, 14, 27, 30, 33, 11, 45	f1otrgitv 27812	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)) ↔ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑑)))))
47	43, 46	mpbird 256	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)))
48		simpr3 1196	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))
49	16, 41	oveq12d 7375	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘(^◡𝐹‘𝑐))𝐼(𝐹‘(^◡𝐹‘𝑑))) = (𝑐𝐼𝑑))
50	48, 49	eleqtrrd 2841	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑣) ∈ ((𝐹‘(^◡𝐹‘𝑐))𝐼(𝐹‘(^◡𝐹‘𝑑))))
51		simplr3 1217	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑣 ∈ 𝐵)
52	51	ad3antrrr 728	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑣 ∈ 𝐵)
53	19, 20, 21, 22, 23, 24, 14, 27, 30, 9, 11, 52	f1otrgitv 27812	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)) ↔ (𝐹‘𝑣) ∈ ((𝐹‘(^◡𝐹‘𝑐))𝐼(𝐹‘(^◡𝐹‘𝑑)))))
54	50, 53	mpbird 256	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))
55		oveq2 7365	. . . . . . . . . 10 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑥𝐽𝑎) = (𝑥𝐽(^◡𝐹‘𝑐)))
56	55	eleq2d 2823	. . . . . . . . 9 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑦 ∈ (𝑥𝐽𝑎) ↔ 𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐))))
57		oveq1 7364	. . . . . . . . . 10 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑎𝐽𝑏) = ((^◡𝐹‘𝑐)𝐽𝑏))
58	57	eleq2d 2823	. . . . . . . . 9 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑣 ∈ (𝑎𝐽𝑏) ↔ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏)))
59	56, 58	3anbi13d 1438	. . . . . . . 8 ⊢ (𝑎 = (^◡𝐹‘𝑐) → ((𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏))))
60		oveq2 7365	. . . . . . . . . 10 ⊢ (𝑏 = (^◡𝐹‘𝑑) → (𝑥𝐽𝑏) = (𝑥𝐽(^◡𝐹‘𝑑)))
61	60	eleq2d 2823	. . . . . . . . 9 ⊢ (𝑏 = (^◡𝐹‘𝑑) → (𝑧 ∈ (𝑥𝐽𝑏) ↔ 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑))))
62		oveq2 7365	. . . . . . . . . 10 ⊢ (𝑏 = (^◡𝐹‘𝑑) → ((^◡𝐹‘𝑐)𝐽𝑏) = ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))
63	62	eleq2d 2823	. . . . . . . . 9 ⊢ (𝑏 = (^◡𝐹‘𝑑) → (𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏) ↔ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑))))
64	61, 63	3anbi23d 1439	. . . . . . . 8 ⊢ (𝑏 = (^◡𝐹‘𝑑) → ((𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))))
65	59, 64	rspc2ev 3592	. . . . . . 7 ⊢ (((^◡𝐹‘𝑐) ∈ 𝐵 ∧ (^◡𝐹‘𝑑) ∈ 𝐵 ∧ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))
66	9, 11, 38, 47, 54, 65	syl113anc 1382	. . . . . 6 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))
67		f1otrge.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ TarskiG_E)
68	67	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐺 ∈ TarskiG_E)
69		f1of 6784	. . . . . . . . . . 11 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵⟶𝑃)
70	3, 69	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵⟶𝑃)
71	70	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹:𝐵⟶𝑃)
72	71, 31	ffvelcdmd 7036	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑥) ∈ 𝑃)
73	72	ad2antrr 724	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑥) ∈ 𝑃)
74	71, 34	ffvelcdmd 7036	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑦) ∈ 𝑃)
75	74	ad2antrr 724	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑦) ∈ 𝑃)
76	70	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐹:𝐵⟶𝑃)
77	76, 44	ffvelcdmd 7036	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑧) ∈ 𝑃)
78		simplr2 1216	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ 𝐵)
79	76, 78	ffvelcdmd 7036	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ 𝑃)
80	76, 51	ffvelcdmd 7036	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑣) ∈ 𝑃)
81		simpr1 1194	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ (𝑥𝐽𝑣))
82	19, 20, 21, 22, 23, 24, 13, 26, 29, 32, 51, 78	f1otrgitv 27812	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝑢 ∈ (𝑥𝐽𝑣) ↔ (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑣))))
83	81, 82	mpbid 231	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑣)))
84		simpr2 1195	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ (𝑦𝐽𝑧))
85	19, 20, 21, 22, 23, 24, 13, 26, 29, 35, 44, 78	f1otrgitv 27812	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝑢 ∈ (𝑦𝐽𝑧) ↔ (𝐹‘𝑢) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧))))
86	84, 85	mpbid 231	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧)))
87		simpr3 1196	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑥 ≠ 𝑢)
88		dff1o6 7221	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵–1-1-onto→𝑃 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀𝑥 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢)))
89	88	simp3bi 1147	. . . . . . . . . . . 12 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → ∀𝑥 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢))
90	89	r19.21bi 3234	. . . . . . . . . . 11 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) → ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢))
91	90	r19.21bi 3234	. . . . . . . . . 10 ⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢))
92	91	necon3d 2964	. . . . . . . . 9 ⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → (𝑥 ≠ 𝑢 → (𝐹‘𝑥) ≠ (𝐹‘𝑢)))
93	92	imp 407	. . . . . . . 8 ⊢ ((((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ≠ 𝑢) → (𝐹‘𝑥) ≠ (𝐹‘𝑢))
94	13, 32, 78, 87, 93	syl1111anc 838	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑥) ≠ (𝐹‘𝑢))
95	19, 20, 21, 68, 73, 75, 77, 79, 80, 83, 86, 94	axtgeucl 27414	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑)))
96	66, 95	r19.29vva 3207	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))
97	96	ex 413	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))))
98	97	ralrimivvva 3200	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))))
99	98	ralrimivva 3197	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))))
100	22, 23, 24	istrkge 27399	. 2 ⊢ (𝐻 ∈ TarskiG_E ↔ (𝐻 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))))
101	2, 99, 100	sylanbrc 583	1 ⊢ (𝜑 → 𝐻 ∈ TarskiG_E)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3073 Vcvv 3445 ^◡ccnv 5632 ran crn 5634 Fn wfn 6491 ⟶wf 6492 –1-1-onto→wf1o 6495 ‘cfv 6496 (class class class)co 7357 Basecbs 17083 distcds 17142 TarskiG_Ecstrkge 27374 Itvcitv 27375

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2944 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-sbc 3740 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-ov 7360 df-trkge 27393

This theorem is referenced by: (None)

W3C validator