f1otrge

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)

	Ref	Expression
Hypotheses	f1otrkg.p	$⊢ P = {Base}_{G}$
	f1otrkg.d	$⊢ D = dist (G)$
	f1otrkg.i	$⊢ I = Itv (G)$
	f1otrkg.b	$⊢ B = {Base}_{H}$
	f1otrkg.e	$⊢ E = dist (H)$
	f1otrkg.j	$⊢ J = Itv (H)$
	f1otrkg.f	$⊢ φ \to F : B \underset{1-1 onto}{⟶} P$
	f1otrkg.1	$⊢ (φ \land (e \in B \land f \in B)) \to e E f = F (e) D F (f)$
	f1otrkg.2	$⊢ (φ \land (e \in B \land f \in B \land g \in B)) \to (g \in (e J f) \leftrightarrow F (g) \in (F (e) I F (f)))$
	f1otrg.h	$⊢ φ \to H \in V$
	f1otrge.g	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
Assertion	f1otrge	$⊢ φ \to H \in 𝒢_{Tarski}^{E}$

Proof

Step	Hyp	Ref	Expression
1		f1otrkg.p	$⊢ P = {Base}_{G}$
2		f1otrkg.d	$⊢ D = dist (G)$
3		f1otrkg.i	$⊢ I = Itv (G)$
4		f1otrkg.b	$⊢ B = {Base}_{H}$
5		f1otrkg.e	$⊢ E = dist (H)$
6		f1otrkg.j	$⊢ J = Itv (H)$
7		f1otrkg.f	$⊢ φ \to F : B \underset{1-1 onto}{⟶} P$
8		f1otrkg.1	$⊢ (φ \land (e \in B \land f \in B)) \to e E f = F (e) D F (f)$
9		f1otrkg.2	$⊢ (φ \land (e \in B \land f \in B \land g \in B)) \to (g \in (e J f) \leftrightarrow F (g) \in (F (e) I F (f)))$
10		f1otrg.h	$⊢ φ \to H \in V$
11		f1otrge.g	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
12	10	elexd	$⊢ φ \to H \in V$
13		f1ocnv	$⊢ F : B \underset{1-1 onto}{⟶} P \to F^{-1} : P \underset{1-1 onto}{⟶} B$
14		f1of	$⊢ F^{-1} : P \underset{1-1 onto}{⟶} B \to F^{-1} : P ⟶ B$
15	7 13 14	3syl	$⊢ φ \to F^{-1} : P ⟶ B$
16	15	ad6antr	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F^{-1} : P ⟶ B$
17		simpllr	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to c \in P$
18	16 17	ffvelrnd	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F^{-1} (c) \in B$
19		simplr	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to d \in P$
20	16 19	ffvelrnd	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F^{-1} (d) \in B$
21		simpr1	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F (y) \in (F (x) I c)$
22	7	ad3antrrr	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to F : B \underset{1-1 onto}{⟶} P$
23	22	ad3antrrr	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F : B \underset{1-1 onto}{⟶} P$
24		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} P \land c \in P) \to F (F^{-1} (c)) = c$
25	23 17 24	syl2anc	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F (F^{-1} (c)) = c$
26	25	oveq2d	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F (x) I F (F^{-1} (c)) = F (x) I c$
27	21 26	eleqtrrd	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F (y) \in (F (x) I F (F^{-1} (c)))$
28	8	ad5ant15	$⊢ ((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land (e \in B \land f \in B)) \to e E f = F (e) D F (f)$
29	28	ad5ant15	$⊢ (((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \land (e \in B \land f \in B)) \to e E f = F (e) D F (f)$
30	9	ad5ant15	$⊢ ((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land (e \in B \land f \in B \land g \in B)) \to (g \in (e J f) \leftrightarrow F (g) \in (F (e) I F (f)))$
31	30	ad5ant15	$⊢ (((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \land (e \in B \land f \in B \land g \in B)) \to (g \in (e J f) \leftrightarrow F (g) \in (F (e) I F (f)))$
32		simprl	$⊢ (φ \land (x \in B \land y \in B)) \to x \in B$
33	32	ad2antrr	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to x \in B$
34	33	ad3antrrr	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to x \in B$
35		simprr	$⊢ (φ \land (x \in B \land y \in B)) \to y \in B$
36	35	ad2antrr	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to y \in B$
37	36	ad3antrrr	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to y \in B$
38	1 2 3 4 5 6 23 29 31 34 18 37	f1otrgitv	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to (y \in (x J F^{-1} (c)) \leftrightarrow F (y) \in (F (x) I F (F^{-1} (c))))$
39	27 38	mpbird	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to y \in (x J F^{-1} (c))$
40		simpr2	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F (z) \in (F (x) I d)$
41		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} P \land d \in P) \to F (F^{-1} (d)) = d$
42	23 19 41	syl2anc	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F (F^{-1} (d)) = d$
43	42	oveq2d	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F (x) I F (F^{-1} (d)) = F (x) I d$
44	40 43	eleqtrrd	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F (z) \in (F (x) I F (F^{-1} (d)))$
45		simplr1	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to z \in B$
46	45	ad3antrrr	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to z \in B$
47	1 2 3 4 5 6 23 29 31 34 20 46	f1otrgitv	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to (z \in (x J F^{-1} (d)) \leftrightarrow F (z) \in (F (x) I F (F^{-1} (d))))$
48	44 47	mpbird	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to z \in (x J F^{-1} (d))$
49		simpr3	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F (v) \in (c I d)$
50	25 42	oveq12d	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F (F^{-1} (c)) I F (F^{-1} (d)) = c I d$
51	49 50	eleqtrrd	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to F (v) \in (F (F^{-1} (c)) I F (F^{-1} (d)))$
52		simplr3	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to v \in B$
53	52	ad3antrrr	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to v \in B$
54	1 2 3 4 5 6 23 29 31 18 20 53	f1otrgitv	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to (v \in (F^{-1} (c) J F^{-1} (d)) \leftrightarrow F (v) \in (F (F^{-1} (c)) I F (F^{-1} (d))))$
55	51 54	mpbird	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to v \in (F^{-1} (c) J F^{-1} (d))$
56		oveq2	$⊢ a = F^{-1} (c) \to x J a = x J F^{-1} (c)$
57	56	eleq2d	$⊢ a = F^{-1} (c) \to (y \in (x J a) \leftrightarrow y \in (x J F^{-1} (c)))$
58		oveq1	$⊢ a = F^{-1} (c) \to a J b = F^{-1} (c) J b$
59	58	eleq2d	$⊢ a = F^{-1} (c) \to (v \in (a J b) \leftrightarrow v \in (F^{-1} (c) J b))$
60	57 59	3anbi13d	$⊢ a = F^{-1} (c) \to ((y \in (x J a) \land z \in (x J b) \land v \in (a J b)) \leftrightarrow (y \in (x J F^{-1} (c)) \land z \in (x J b) \land v \in (F^{-1} (c) J b)))$
61		oveq2	$⊢ b = F^{-1} (d) \to x J b = x J F^{-1} (d)$
62	61	eleq2d	$⊢ b = F^{-1} (d) \to (z \in (x J b) \leftrightarrow z \in (x J F^{-1} (d)))$
63		oveq2	$⊢ b = F^{-1} (d) \to F^{-1} (c) J b = F^{-1} (c) J F^{-1} (d)$
64	63	eleq2d	$⊢ b = F^{-1} (d) \to (v \in (F^{-1} (c) J b) \leftrightarrow v \in (F^{-1} (c) J F^{-1} (d)))$
65	62 64	3anbi23d	$⊢ b = F^{-1} (d) \to ((y \in (x J F^{-1} (c)) \land z \in (x J b) \land v \in (F^{-1} (c) J b)) \leftrightarrow (y \in (x J F^{-1} (c)) \land z \in (x J F^{-1} (d)) \land v \in (F^{-1} (c) J F^{-1} (d))))$
66	60 65	rspc2ev	$⊢ (F^{-1} (c) \in B \land F^{-1} (d) \in B \land (y \in (x J F^{-1} (c)) \land z \in (x J F^{-1} (d)) \land v \in (F^{-1} (c) J F^{-1} (d)))) \to \exists a \in B \exists b \in B (y \in (x J a) \land z \in (x J b) \land v \in (a J b))$
67	18 20 39 48 55 66	syl113anc	$⊢ ((((((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \land c \in P) \land d \in P) \land (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))) \to \exists a \in B \exists b \in B (y \in (x J a) \land z \in (x J b) \land v \in (a J b))$
68	11	ad3antrrr	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to G \in 𝒢_{Tarski}^{E}$
69		f1of	$⊢ F : B \underset{1-1 onto}{⟶} P \to F : B ⟶ P$
70	7 69	syl	$⊢ φ \to F : B ⟶ P$
71	70	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to F : B ⟶ P$
72	71 32	ffvelrnd	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) \in P$
73	72	ad2antrr	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to F (x) \in P$
74	71 35	ffvelrnd	$⊢ (φ \land (x \in B \land y \in B)) \to F (y) \in P$
75	74	ad2antrr	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to F (y) \in P$
76	70	ad3antrrr	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to F : B ⟶ P$
77	76 45	ffvelrnd	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to F (z) \in P$
78		simplr2	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to u \in B$
79	76 78	ffvelrnd	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to F (u) \in P$
80	76 52	ffvelrnd	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to F (v) \in P$
81		simpr1	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to u \in (x J v)$
82	1 2 3 4 5 6 22 28 30 33 52 78	f1otrgitv	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to (u \in (x J v) \leftrightarrow F (u) \in (F (x) I F (v)))$
83	81 82	mpbid	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to F (u) \in (F (x) I F (v))$
84		simpr2	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to u \in (y J z)$
85	1 2 3 4 5 6 22 28 30 36 45 78	f1otrgitv	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to (u \in (y J z) \leftrightarrow F (u) \in (F (y) I F (z)))$
86	84 85	mpbid	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to F (u) \in (F (y) I F (z))$
87		simpr3	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to x \neq u$
88		dff1o6	$⊢ F : B \underset{1-1 onto}{⟶} P \leftrightarrow (F Fn B \land ran F = P \land \forall x \in B \forall u \in B (F (x) = F (u) \to x = u))$
89	88	simp3bi	$⊢ F : B \underset{1-1 onto}{⟶} P \to \forall x \in B \forall u \in B (F (x) = F (u) \to x = u)$
90	89	r19.21bi	$⊢ (F : B \underset{1-1 onto}{⟶} P \land x \in B) \to \forall u \in B (F (x) = F (u) \to x = u)$
91	90	r19.21bi	$⊢ ((F : B \underset{1-1 onto}{⟶} P \land x \in B) \land u \in B) \to (F (x) = F (u) \to x = u)$
92	91	necon3d	$⊢ ((F : B \underset{1-1 onto}{⟶} P \land x \in B) \land u \in B) \to (x \neq u \to F (x) \neq F (u))$
93	92	imp	$⊢ (((F : B \underset{1-1 onto}{⟶} P \land x \in B) \land u \in B) \land x \neq u) \to F (x) \neq F (u)$
94	22 33 78 87 93	syl1111anc	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to F (x) \neq F (u)$
95	1 2 3 68 73 75 77 79 80 83 86 94	axtgeucl	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to \exists c \in P \exists d \in P (F (y) \in (F (x) I c) \land F (z) \in (F (x) I d) \land F (v) \in (c I d))$
96	67 95	r19.29vva	$⊢ (((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \land (u \in (x J v) \land u \in (y J z) \land x \neq u)) \to \exists a \in B \exists b \in B (y \in (x J a) \land z \in (x J b) \land v \in (a J b))$
97	96	ex	$⊢ ((φ \land (x \in B \land y \in B)) \land (z \in B \land u \in B \land v \in B)) \to ((u \in (x J v) \land u \in (y J z) \land x \neq u) \to \exists a \in B \exists b \in B (y \in (x J a) \land z \in (x J b) \land v \in (a J b)))$
98	97	ralrimivvva	$⊢ (φ \land (x \in B \land y \in B)) \to \forall z \in B \forall u \in B \forall v \in B ((u \in (x J v) \land u \in (y J z) \land x \neq u) \to \exists a \in B \exists b \in B (y \in (x J a) \land z \in (x J b) \land v \in (a J b)))$
99	98	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B \forall z \in B \forall u \in B \forall v \in B ((u \in (x J v) \land u \in (y J z) \land x \neq u) \to \exists a \in B \exists b \in B (y \in (x J a) \land z \in (x J b) \land v \in (a J b)))$
100	4 5 6	istrkge	$⊢ H \in 𝒢_{Tarski}^{E} \leftrightarrow (H \in V \land \forall x \in B \forall y \in B \forall z \in B \forall u \in B \forall v \in B ((u \in (x J v) \land u \in (y J z) \land x \neq u) \to \exists a \in B \exists b \in B (y \in (x J a) \land z \in (x J b) \land v \in (a J b))))$
101	12 99 100	sylanbrc	$⊢ φ \to H \in 𝒢_{Tarski}^{E}$

Metamath Proof Explorer

Theorem f1otrge

Proof