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 25752

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		elex 3212	. . 3 ⊢ (𝐻 ∈ 𝑉 → 𝐻 ∈ V)
3	1, 2	syl 17	. 2 ⊢ (𝜑 → 𝐻 ∈ V)
4		f1otrkg.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃)
5		f1ocnv 6149	. . . . . . . . . 10 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → ^◡𝐹:𝑃–1-1-onto→𝐵)
6		f1of 6137	. . . . . . . . . 10 ⊢ (^◡𝐹:𝑃–1-1-onto→𝐵 → ^◡𝐹:𝑃⟶𝐵)
7	4, 5, 6	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ^◡𝐹:𝑃⟶𝐵)
8	7	ad6antr 772	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ^◡𝐹:𝑃⟶𝐵)
9		simpllr 799	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑐 ∈ 𝑃)
10	8, 9	ffvelrnd 6360	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (^◡𝐹‘𝑐) ∈ 𝐵)
11		simplr 792	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑑 ∈ 𝑃)
12	8, 11	ffvelrnd 6360	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (^◡𝐹‘𝑑) ∈ 𝐵)
13		simpr1 1067	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐))
14	4	ad3antrrr 766	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐹:𝐵–1-1-onto→𝑃)
15	14	ad3antrrr 766	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝐹:𝐵–1-1-onto→𝑃)
16		f1ocnvfv2 6533	. . . . . . . . . . 11 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → (𝐹‘(^◡𝐹‘𝑐)) = 𝑐)
17	15, 9, 16	syl2anc 693	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘(^◡𝐹‘𝑐)) = 𝑐)
18	17	oveq2d 6666	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑐))) = ((𝐹‘𝑥)𝐼𝑐))
19	13, 18	eleqtrrd 2704	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑐))))
20		f1otrkg.p	. . . . . . . . 9 ⊢ 𝑃 = (Base‘𝐺)
21		f1otrkg.d	. . . . . . . . 9 ⊢ 𝐷 = (dist‘𝐺)
22		f1otrkg.i	. . . . . . . . 9 ⊢ 𝐼 = (Itv‘𝐺)
23		f1otrkg.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐻)
24		f1otrkg.e	. . . . . . . . 9 ⊢ 𝐸 = (dist‘𝐻)
25		f1otrkg.j	. . . . . . . . 9 ⊢ 𝐽 = (Itv‘𝐻)
26		simp-4l 806	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)))
27		simplll 798	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
28		f1otrkg.1	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
29	28	adantlr 751	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
30	27, 29	sylancom 701	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
31	26, 30	sylancom 701	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))
32		simp-4l 806	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)))
33		simplll 798	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
34		f1otrkg.2	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
35	34	adantlr 751	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
36	33, 35	sylancom 701	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
37	32, 36	sylancom 701	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))
38		simprl 794	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵)
39	38	ad2antrr 762	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑥 ∈ 𝐵)
40	39	ad3antrrr 766	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑥 ∈ 𝐵)
41		simprr 796	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵)
42	41	ad2antrr 762	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑦 ∈ 𝐵)
43	42	ad3antrrr 766	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑦 ∈ 𝐵)
44	20, 21, 22, 23, 24, 25, 15, 31, 37, 40, 10, 43	f1otrgitv 25750	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑐)))))
45	19, 44	mpbird 247	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)))
46		simpr2 1068	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑))
47		f1ocnvfv2 6533	. . . . . . . . . . 11 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑑 ∈ 𝑃) → (𝐹‘(^◡𝐹‘𝑑)) = 𝑑)
48	15, 11, 47	syl2anc 693	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘(^◡𝐹‘𝑑)) = 𝑑)
49	48	oveq2d 6666	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑑))) = ((𝐹‘𝑥)𝐼𝑑))
50	46, 49	eleqtrrd 2704	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑑))))
51		simplr1 1103	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑧 ∈ 𝐵)
52	51	ad3antrrr 766	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑧 ∈ 𝐵)
53	20, 21, 22, 23, 24, 25, 15, 31, 37, 40, 12, 52	f1otrgitv 25750	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)) ↔ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(^◡𝐹‘𝑑)))))
54	50, 53	mpbird 247	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)))
55		simpr3 1069	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))
56	17, 48	oveq12d 6668	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘(^◡𝐹‘𝑐))𝐼(𝐹‘(^◡𝐹‘𝑑))) = (𝑐𝐼𝑑))
57	55, 56	eleqtrrd 2704	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑣) ∈ ((𝐹‘(^◡𝐹‘𝑐))𝐼(𝐹‘(^◡𝐹‘𝑑))))
58		simplr3 1105	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑣 ∈ 𝐵)
59	58	ad3antrrr 766	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑣 ∈ 𝐵)
60	20, 21, 22, 23, 24, 25, 15, 31, 37, 10, 12, 59	f1otrgitv 25750	. . . . . . . 8 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)) ↔ (𝐹‘𝑣) ∈ ((𝐹‘(^◡𝐹‘𝑐))𝐼(𝐹‘(^◡𝐹‘𝑑)))))
61	57, 60	mpbird 247	. . . . . . 7 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))
62		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑥𝐽𝑎) = (𝑥𝐽(^◡𝐹‘𝑐)))
63	62	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑦 ∈ (𝑥𝐽𝑎) ↔ 𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐))))
64		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑎𝐽𝑏) = ((^◡𝐹‘𝑐)𝐽𝑏))
65	64	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑎 = (^◡𝐹‘𝑐) → (𝑣 ∈ (𝑎𝐽𝑏) ↔ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏)))
66	63, 65	3anbi13d 1401	. . . . . . . 8 ⊢ (𝑎 = (^◡𝐹‘𝑐) → ((𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏))))
67		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑏 = (^◡𝐹‘𝑑) → (𝑥𝐽𝑏) = (𝑥𝐽(^◡𝐹‘𝑑)))
68	67	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑏 = (^◡𝐹‘𝑑) → (𝑧 ∈ (𝑥𝐽𝑏) ↔ 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑))))
69		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑏 = (^◡𝐹‘𝑑) → ((^◡𝐹‘𝑐)𝐽𝑏) = ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))
70	69	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑏 = (^◡𝐹‘𝑑) → (𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏) ↔ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑))))
71	68, 70	3anbi23d 1402	. . . . . . . 8 ⊢ (𝑏 = (^◡𝐹‘𝑑) → ((𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))))
72	66, 71	rspc2ev 3324	. . . . . . 7 ⊢ (((^◡𝐹‘𝑐) ∈ 𝐵 ∧ (^◡𝐹‘𝑑) ∈ 𝐵 ∧ (𝑦 ∈ (𝑥𝐽(^◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽(^◡𝐹‘𝑑)) ∧ 𝑣 ∈ ((^◡𝐹‘𝑐)𝐽(^◡𝐹‘𝑑)))) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))
73	10, 12, 45, 54, 61, 72	syl113anc 1338	. . . . . 6 ⊢ (((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))
74		f1otrge.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ TarskiG_E)
75	74	ad3antrrr 766	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐺 ∈ TarskiG_E)
76		f1of 6137	. . . . . . . . . . 11 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵⟶𝑃)
77	4, 76	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵⟶𝑃)
78	77	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹:𝐵⟶𝑃)
79	78, 38	ffvelrnd 6360	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑥) ∈ 𝑃)
80	79	ad2antrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑥) ∈ 𝑃)
81	78, 41	ffvelrnd 6360	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑦) ∈ 𝑃)
82	81	ad2antrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑦) ∈ 𝑃)
83	77	ad3antrrr 766	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐹:𝐵⟶𝑃)
84	83, 51	ffvelrnd 6360	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑧) ∈ 𝑃)
85		simplr2 1104	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ 𝐵)
86	83, 85	ffvelrnd 6360	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ 𝑃)
87	83, 58	ffvelrnd 6360	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑣) ∈ 𝑃)
88		simpr1 1067	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ (𝑥𝐽𝑣))
89	20, 21, 22, 23, 24, 25, 14, 30, 36, 39, 58, 85	f1otrgitv 25750	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝑢 ∈ (𝑥𝐽𝑣) ↔ (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑣))))
90	88, 89	mpbid 222	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑣)))
91		simpr2 1068	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ (𝑦𝐽𝑧))
92	20, 21, 22, 23, 24, 25, 14, 30, 36, 42, 51, 85	f1otrgitv 25750	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝑢 ∈ (𝑦𝐽𝑧) ↔ (𝐹‘𝑢) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧))))
93	91, 92	mpbid 222	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧)))
94	14, 39	jca 554	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵))
95		simpr3 1069	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑥 ≠ 𝑢)
96		dff1o6 6531	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵–1-1-onto→𝑃 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀𝑥 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢)))
97	96	simp3bi 1078	. . . . . . . . . . . 12 ⊢ (𝐹:𝐵–1-1-onto→𝑃 → ∀𝑥 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢))
98	97	r19.21bi 2932	. . . . . . . . . . 11 ⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) → ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢))
99	98	r19.21bi 2932	. . . . . . . . . 10 ⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢))
100	99	necon3d 2815	. . . . . . . . 9 ⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → (𝑥 ≠ 𝑢 → (𝐹‘𝑥) ≠ (𝐹‘𝑢)))
101	100	imp 445	. . . . . . . 8 ⊢ ((((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ≠ 𝑢) → (𝐹‘𝑥) ≠ (𝐹‘𝑢))
102	94, 85, 95, 101	syl21anc 1325	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑥) ≠ (𝐹‘𝑢))
103	20, 21, 22, 75, 80, 82, 84, 86, 87, 90, 93, 102	axtgeucl 25371	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑)))
104	73, 103	r19.29vva 3081	. . . . 5 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))
105	104	ex 450	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))))
106	105	ralrimivvva 2972	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))))
107	106	ralrimivva 2971	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))))
108	23, 24, 25	istrkge 25356	. 2 ⊢ (𝐻 ∈ TarskiG_E ↔ (𝐻 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))))
109	3, 107, 108	sylanbrc 698	1 ⊢ (𝜑 → 𝐻 ∈ TarskiG_E)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 Vcvv 3200 ^◡ccnv 5113 ran crn 5115 Fn wfn 5883 ⟶wf 5884 –1-1-onto→wf1o 5887 ‘cfv 5888 (class class class)co 6650 Basecbs 15857 distcds 15950 TarskiG_Ecstrkge 25334 Itvcitv 25335

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-ov 6653 df-trkge 25350

This theorem is referenced by: (None)

W3C validator