f1otrg

Description: A bijection between bases which conserves distances and intervals conserves also geometries. (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$
	f1otrg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	f1otrg.l	$⊢ φ \to {Line}_{𝒢} (H) = (x \in B, y \in (B ∖ \{x\}) ⟼ \{z \in B \| (z \in (x J y) \lor x \in (z J y) \lor y \in (x J z))\})$
Assertion	f1otrg	$⊢ φ \to H \in 𝒢_{Tarski}$

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		f1otrg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
12		f1otrg.l	$⊢ φ \to {Line}_{𝒢} (H) = (x \in B, y \in (B ∖ \{x\}) ⟼ \{z \in B \| (z \in (x J y) \lor x \in (z J y) \lor y \in (x J z))\})$
13	10	elexd	$⊢ φ \to H \in V$
14	11	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to G \in 𝒢_{Tarski}$
15		f1of	$⊢ F : B \underset{1-1 onto}{⟶} P \to F : B ⟶ P$
16	7 15	syl	$⊢ φ \to F : B ⟶ P$
17	16	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to F : B ⟶ P$
18		simprl	$⊢ (φ \land (x \in B \land y \in B)) \to x \in B$
19	17 18	ffvelrnd	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) \in P$
20		simprr	$⊢ (φ \land (x \in B \land y \in B)) \to y \in B$
21	17 20	ffvelrnd	$⊢ (φ \land (x \in B \land y \in B)) \to F (y) \in P$
22	1 2 3 14 19 21	axtgcgrrflx	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) D F (y) = F (y) D F (x)$
23	7	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to F : B \underset{1-1 onto}{⟶} P$
24	8	adantlr	$⊢ ((φ \land (x \in B \land y \in B)) \land (e \in B \land f \in B)) \to e E f = F (e) D F (f)$
25	9	adantlr	$⊢ ((φ \land (x \in B \land y \in B)) \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)))$
26	1 2 3 4 5 6 23 24 25 18 20	f1otrgds	$⊢ (φ \land (x \in B \land y \in B)) \to x E y = F (x) D F (y)$
27	1 2 3 4 5 6 23 24 25 20 18	f1otrgds	$⊢ (φ \land (x \in B \land y \in B)) \to y E x = F (y) D F (x)$
28	22 26 27	3eqtr4d	$⊢ (φ \land (x \in B \land y \in B)) \to x E y = y E x$
29	28	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B x E y = y E x$
30		f1of1	$⊢ F : B \underset{1-1 onto}{⟶} P \to F : B \underset{1-1}{⟶} P$
31	7 30	syl	$⊢ φ \to F : B \underset{1-1}{⟶} P$
32	31	3ad2ant1	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to F : B \underset{1-1}{⟶} P$
33		simp21	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to x \in B$
34		simp22	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to y \in B$
35	33 34	jca	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to (x \in B \land y \in B)$
36	11	3ad2ant1	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to G \in 𝒢_{Tarski}$
37	16	3ad2ant1	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to F : B ⟶ P$
38	37 33	ffvelrnd	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to F (x) \in P$
39	37 34	ffvelrnd	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to F (y) \in P$
40		simp23	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to z \in B$
41	37 40	ffvelrnd	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to F (z) \in P$
42		simp3	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to x E y = z E z$
43	7	3ad2ant1	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to F : B \underset{1-1 onto}{⟶} P$
44	8	3ad2antl1	$⊢ ((φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \land (e \in B \land f \in B)) \to e E f = F (e) D F (f)$
45	9	3ad2antl1	$⊢ ((φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \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)))$
46	1 2 3 4 5 6 43 44 45 33 34	f1otrgds	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to x E y = F (x) D F (y)$
47	1 2 3 4 5 6 43 44 45 40 40	f1otrgds	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to z E z = F (z) D F (z)$
48	42 46 47	3eqtr3d	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to F (x) D F (y) = F (z) D F (z)$
49	1 2 3 36 38 39 41 48	axtgcgrid	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to F (x) = F (y)$
50		f1veqaeq	$⊢ (F : B \underset{1-1}{⟶} P \land (x \in B \land y \in B)) \to (F (x) = F (y) \to x = y)$
51	50	imp	$⊢ ((F : B \underset{1-1}{⟶} P \land (x \in B \land y \in B)) \land F (x) = F (y)) \to x = y$
52	32 35 49 51	syl21anc	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land x E y = z E z) \to x = y$
53	52	3expia	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x E y = z E z \to x = y)$
54	53	ralrimivvva	$⊢ φ \to \forall x \in B \forall y \in B \forall z \in B (x E y = z E z \to x = y)$
55	29 54	jca	$⊢ φ \to (\forall x \in B \forall y \in B x E y = y E x \land \forall x \in B \forall y \in B \forall z \in B (x E y = z E z \to x = y))$
56	4 5 6	istrkgc	$⊢ H \in 𝒢_{Tarski}^{C} \leftrightarrow (H \in V \land (\forall x \in B \forall y \in B x E y = y E x \land \forall x \in B \forall y \in B \forall z \in B (x E y = z E z \to x = y)))$
57	13 55 56	sylanbrc	$⊢ φ \to H \in 𝒢_{Tarski}^{C}$
58	7	3ad2ant1	$⊢ (φ \land (x \in B \land y \in B) \land y \in (x J x)) \to F : B \underset{1-1 onto}{⟶} P$
59	58 30	syl	$⊢ (φ \land (x \in B \land y \in B) \land y \in (x J x)) \to F : B \underset{1-1}{⟶} P$
60		simp2	$⊢ (φ \land (x \in B \land y \in B) \land y \in (x J x)) \to (x \in B \land y \in B)$
61	11	3ad2ant1	$⊢ (φ \land (x \in B \land y \in B) \land y \in (x J x)) \to G \in 𝒢_{Tarski}$
62	19	3adant3	$⊢ (φ \land (x \in B \land y \in B) \land y \in (x J x)) \to F (x) \in P$
63	21	3adant3	$⊢ (φ \land (x \in B \land y \in B) \land y \in (x J x)) \to F (y) \in P$
64		simp3	$⊢ (φ \land (x \in B \land y \in B) \land y \in (x J x)) \to y \in (x J x)$
65	8	3ad2antl1	$⊢ ((φ \land (x \in B \land y \in B) \land y \in (x J x)) \land (e \in B \land f \in B)) \to e E f = F (e) D F (f)$
66	9	3ad2antl1	$⊢ ((φ \land (x \in B \land y \in B) \land y \in (x J x)) \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)))$
67	18	3adant3	$⊢ (φ \land (x \in B \land y \in B) \land y \in (x J x)) \to x \in B$
68	20	3adant3	$⊢ (φ \land (x \in B \land y \in B) \land y \in (x J x)) \to y \in B$
69	1 2 3 4 5 6 58 65 66 67 67 68	f1otrgitv	$⊢ (φ \land (x \in B \land y \in B) \land y \in (x J x)) \to (y \in (x J x) \leftrightarrow F (y) \in (F (x) I F (x)))$
70	64 69	mpbid	$⊢ (φ \land (x \in B \land y \in B) \land y \in (x J x)) \to F (y) \in (F (x) I F (x))$
71	1 2 3 61 62 63 70	axtgbtwnid	$⊢ (φ \land (x \in B \land y \in B) \land y \in (x J x)) \to F (x) = F (y)$
72	59 60 71 51	syl21anc	$⊢ (φ \land (x \in B \land y \in B) \land y \in (x J x)) \to x = y$
73	72	3expia	$⊢ (φ \land (x \in B \land y \in B)) \to (y \in (x J x) \to x = y)$
74	73	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B (y \in (x J x) \to x = y)$
75		f1ocnv	$⊢ F : B \underset{1-1 onto}{⟶} P \to F^{-1} : P \underset{1-1 onto}{⟶} B$
76		f1of	$⊢ F^{-1} : P \underset{1-1 onto}{⟶} B \to F^{-1} : P ⟶ B$
77	7 75 76	3syl	$⊢ φ \to F^{-1} : P ⟶ B$
78	77	ad5antr	$⊢ (((((φ \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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to F^{-1} : P ⟶ B$
79		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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to c \in P$
80	78 79	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to F^{-1} (c) \in B$
81		simpr	$⊢ ((((((φ \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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \land a = F^{-1} (c)) \to a = F^{-1} (c)$
82	81	eleq1d	$⊢ ((((((φ \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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \land a = F^{-1} (c)) \to (a \in (u J y) \leftrightarrow F^{-1} (c) \in (u J y))$
83	81	eleq1d	$⊢ ((((((φ \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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \land a = F^{-1} (c)) \to (a \in (v J x) \leftrightarrow F^{-1} (c) \in (v J x))$
84	82 83	anbi12d	$⊢ ((((((φ \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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \land a = F^{-1} (c)) \to ((a \in (u J y) \land a \in (v J x)) \leftrightarrow (F^{-1} (c) \in (u J y) \land F^{-1} (c) \in (v J x)))$
85		simprl	$⊢ (((((φ \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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to c \in (F (u) I F (y))$
86	23	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 z) \land v \in (y J z))) \to F : B \underset{1-1 onto}{⟶} P$
87	86	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to F : B \underset{1-1 onto}{⟶} P$
88		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} P \land c \in P) \to F (F^{-1} (c)) = c$
89	88	eleq1d	$⊢ (F : B \underset{1-1 onto}{⟶} P \land c \in P) \to (F (F^{-1} (c)) \in (F (u) I F (y)) \leftrightarrow c \in (F (u) I F (y)))$
90	87 79 89	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to (F (F^{-1} (c)) \in (F (u) I F (y)) \leftrightarrow c \in (F (u) I F (y)))$
91	85 90	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to F (F^{-1} (c)) \in (F (u) I F (y))$
92	24	ad4ant14	$⊢ ((((φ \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 z) \land v \in (y J z))) \land (e \in B \land f \in B)) \to e E f = F (e) D F (f)$
93	92	ad4ant14	$⊢ ((((((φ \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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \land (e \in B \land f \in B)) \to e E f = F (e) D F (f)$
94	25	ad4ant14	$⊢ ((((φ \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 z) \land v \in (y J z))) \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)))$
95	94	ad4ant14	$⊢ ((((((φ \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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \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)))$
96		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 z) \land v \in (y J z))) \to u \in B$
97	96	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to u \in B$
98	20	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 z) \land v \in (y J z))) \to y \in B$
99	98	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to y \in B$
100	1 2 3 4 5 6 87 93 95 97 99 80	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to (F^{-1} (c) \in (u J y) \leftrightarrow F (F^{-1} (c)) \in (F (u) I F (y)))$
101	91 100	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to F^{-1} (c) \in (u J y)$
102		simprr	$⊢ (((((φ \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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to c \in (F (v) I F (x))$
103	88	eleq1d	$⊢ (F : B \underset{1-1 onto}{⟶} P \land c \in P) \to (F (F^{-1} (c)) \in (F (v) I F (x)) \leftrightarrow c \in (F (v) I F (x)))$
104	87 79 103	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to (F (F^{-1} (c)) \in (F (v) I F (x)) \leftrightarrow c \in (F (v) I F (x)))$
105	102 104	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to F (F^{-1} (c)) \in (F (v) I F (x))$
106		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 z) \land v \in (y J z))) \to v \in B$
107	106	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to v \in B$
108	18	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 z) \land v \in (y J z))) \to x \in B$
109	108	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to x \in B$
110	1 2 3 4 5 6 87 93 95 107 109 80	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to (F^{-1} (c) \in (v J x) \leftrightarrow F (F^{-1} (c)) \in (F (v) I F (x)))$
111	105 110	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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to F^{-1} (c) \in (v J x)$
112	101 111	jca	$⊢ (((((φ \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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to (F^{-1} (c) \in (u J y) \land F^{-1} (c) \in (v J x))$
113	80 84 112	rspcedvd	$⊢ (((((φ \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 z) \land v \in (y J z))) \land c \in P) \land (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))) \to \exists a \in B (a \in (u J y) \land a \in (v J x))$
114	14	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 z) \land v \in (y J z))) \to G \in 𝒢_{Tarski}$
115	17	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 z) \land v \in (y J z))) \to F : B ⟶ P$
116	115 108	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 z) \land v \in (y J z))) \to F (x) \in P$
117	115 98	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 z) \land v \in (y J z))) \to F (y) \in P$
118		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 z) \land v \in (y J z))) \to z \in B$
119	115 118	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 z) \land v \in (y J z))) \to F (z) \in P$
120	115 96	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 z) \land v \in (y J z))) \to F (u) \in P$
121	115 106	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 z) \land v \in (y J z))) \to F (v) \in P$
122		simprl	$⊢ (((φ \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 z) \land v \in (y J z))) \to u \in (x J z)$
123	1 2 3 4 5 6 86 92 94 108 118 96	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 z) \land v \in (y J z))) \to (u \in (x J z) \leftrightarrow F (u) \in (F (x) I F (z)))$
124	122 123	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 z) \land v \in (y J z))) \to F (u) \in (F (x) I F (z))$
125		simprr	$⊢ (((φ \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 z) \land v \in (y J z))) \to v \in (y J z)$
126	1 2 3 4 5 6 86 92 94 98 118 106	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 z) \land v \in (y J z))) \to (v \in (y J z) \leftrightarrow F (v) \in (F (y) I F (z)))$
127	125 126	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 z) \land v \in (y J z))) \to F (v) \in (F (y) I F (z))$
128	1 2 3 114 116 117 119 120 121 124 127	axtgpasch	$⊢ (((φ \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 z) \land v \in (y J z))) \to \exists c \in P (c \in (F (u) I F (y)) \land c \in (F (v) I F (x)))$
129	113 128	r19.29a	$⊢ (((φ \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 z) \land v \in (y J z))) \to \exists a \in B (a \in (u J y) \land a \in (v J x))$
130	129	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 z) \land v \in (y J z)) \to \exists a \in B (a \in (u J y) \land a \in (v J x)))$
131	130	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 z) \land v \in (y J z)) \to \exists a \in B (a \in (u J y) \land a \in (v J x)))$
132	131	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 z) \land v \in (y J z)) \to \exists a \in B (a \in (u J y) \land a \in (v J x)))$
133	7	ad5antr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to F : B \underset{1-1 onto}{⟶} P$
134		simpllr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to c \in P$
135	133 134 88	syl2anc	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to F (F^{-1} (c)) = c$
136		ffn	$⊢ F : B ⟶ P \to F Fn B$
137	133 15 136	3syl	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to F Fn B$
138		simp-4r	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to (s \in 𝒫 B \land t \in 𝒫 B)$
139	138	simpld	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to s \in 𝒫 B$
140	139	elpwid	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to s \subseteq B$
141	140	adantlr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to s \subseteq B$
142		simprl	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to x \in s$
143		fnfvima	$⊢ (F Fn B \land s \subseteq B \land x \in s) \to F (x) \in F [s]$
144	137 141 142 143	syl3anc	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to F (x) \in F [s]$
145	138	simprd	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to t \in 𝒫 B$
146	145	elpwid	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to t \subseteq B$
147	146	adantlr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to t \subseteq B$
148		simprr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to y \in t$
149		fnfvima	$⊢ (F Fn B \land t \subseteq B \land y \in t) \to F (y) \in F [t]$
150	137 147 148 149	syl3anc	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to F (y) \in F [t]$
151		simplr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to \forall e \in F [s] \forall f \in F [t] c \in (e I f)$
152		oveq1	$⊢ e = F (x) \to e I f = F (x) I f$
153	152	eleq2d	$⊢ e = F (x) \to (c \in (e I f) \leftrightarrow c \in (F (x) I f))$
154		oveq2	$⊢ f = F (y) \to F (x) I f = F (x) I F (y)$
155	154	eleq2d	$⊢ f = F (y) \to (c \in (F (x) I f) \leftrightarrow c \in (F (x) I F (y)))$
156	153 155	rspc2va	$⊢ ((F (x) \in F [s] \land F (y) \in F [t]) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \to c \in (F (x) I F (y))$
157	144 150 151 156	syl21anc	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to c \in (F (x) I F (y))$
158	135 157	eqeltrd	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to F (F^{-1} (c)) \in (F (x) I F (y))$
159	7	ad4antr	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to F : B \underset{1-1 onto}{⟶} P$
160		simp-5l	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \land (e \in B \land f \in B)) \to φ$
161	160 8	sylancom	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \land (e \in B \land f \in B)) \to e E f = F (e) D F (f)$
162		simp-5l	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \land (e \in B \land f \in B \land g \in B)) \to φ$
163	162 9	sylancom	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \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)))$
164		simprl	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to x \in s$
165	140 164	sseldd	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to x \in B$
166		simprr	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to y \in t$
167	146 166	sseldd	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to y \in B$
168	77	ad4antr	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to F^{-1} : P ⟶ B$
169		simplr	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to c \in P$
170	168 169	ffvelrnd	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to F^{-1} (c) \in B$
171	1 2 3 4 5 6 159 161 163 165 167 170	f1otrgitv	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land (x \in s \land y \in t)) \to (F^{-1} (c) \in (x J y) \leftrightarrow F (F^{-1} (c)) \in (F (x) I F (y)))$
172	171	adantlr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to (F^{-1} (c) \in (x J y) \leftrightarrow F (F^{-1} (c)) \in (F (x) I F (y)))$
173	158 172	mpbird	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \land (x \in s \land y \in t)) \to F^{-1} (c) \in (x J y)$
174	173	ralrimivva	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \to \forall x \in s \forall y \in t F^{-1} (c) \in (x J y)$
175	174	adantllr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \to \forall x \in s \forall y \in t F^{-1} (c) \in (x J y)$
176	77	ad4antr	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land c \in P) \to F^{-1} : P ⟶ B$
177		simpr	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land c \in P) \to c \in P$
178	176 177	ffvelrnd	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land c \in P) \to F^{-1} (c) \in B$
179		eleq1	$⊢ b = F^{-1} (c) \to (b \in (x J y) \leftrightarrow F^{-1} (c) \in (x J y))$
180	179	2ralbidv	$⊢ b = F^{-1} (c) \to (\forall x \in s \forall y \in t b \in (x J y) \leftrightarrow \forall x \in s \forall y \in t F^{-1} (c) \in (x J y))$
181	180	adantl	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land c \in P) \land b = F^{-1} (c)) \to (\forall x \in s \forall y \in t b \in (x J y) \leftrightarrow \forall x \in s \forall y \in t F^{-1} (c) \in (x J y))$
182	178 181	rspcedv	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land c \in P) \to (\forall x \in s \forall y \in t F^{-1} (c) \in (x J y) \to \exists b \in B \forall x \in s \forall y \in t b \in (x J y))$
183	182	adantr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \to (\forall x \in s \forall y \in t F^{-1} (c) \in (x J y) \to \exists b \in B \forall x \in s \forall y \in t b \in (x J y))$
184	175 183	mpd	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land c \in P) \land \forall e \in F [s] \forall f \in F [t] c \in (e I f)) \to \exists b \in B \forall x \in s \forall y \in t b \in (x J y)$
185	11	ad3antrrr	$⊢ (((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \to G \in 𝒢_{Tarski}$
186		imassrn	$⊢ F [s] \subseteq ran F$
187		f1ofo	$⊢ F : B \underset{1-1 onto}{⟶} P \to F : B \underset{onto}{⟶} P$
188		forn	$⊢ F : B \underset{onto}{⟶} P \to ran F = P$
189	7 187 188	3syl	$⊢ φ \to ran F = P$
190	189	ad3antrrr	$⊢ (((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \to ran F = P$
191	186 190	sseqtrid	$⊢ (((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \to F [s] \subseteq P$
192		imassrn	$⊢ F [t] \subseteq ran F$
193	192 190	sseqtrid	$⊢ (((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \to F [t] \subseteq P$
194	16	ad3antrrr	$⊢ (((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \to F : B ⟶ P$
195		simplr	$⊢ (((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \to a \in B$
196	194 195	ffvelrnd	$⊢ (((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \to F (a) \in P$
197	7	ad5antr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F : B \underset{1-1 onto}{⟶} P$
198		ffn	$⊢ F^{-1} : P ⟶ B \to F^{-1} Fn P$
199	197 75 76 198	4syl	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F^{-1} Fn P$
200	191	ad2antrr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F [s] \subseteq P$
201		simplr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to u \in F [s]$
202		fnfvima	$⊢ (F^{-1} Fn P \land F [s] \subseteq P \land u \in F [s]) \to F^{-1} (u) \in F^{-1} [F [s]]$
203	199 200 201 202	syl3anc	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F^{-1} (u) \in F^{-1} [F [s]]$
204	197 30	syl	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F : B \underset{1-1}{⟶} P$
205		simp-5r	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to (s \in 𝒫 B \land t \in 𝒫 B)$
206	205	simpld	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to s \in 𝒫 B$
207	206	elpwid	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to s \subseteq B$
208		f1imacnv	$⊢ (F : B \underset{1-1}{⟶} P \land s \subseteq B) \to F^{-1} [F [s]] = s$
209	204 207 208	syl2anc	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F^{-1} [F [s]] = s$
210	203 209	eleqtrd	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F^{-1} (u) \in s$
211	193	ad2antrr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F [t] \subseteq P$
212		simpr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to v \in F [t]$
213		fnfvima	$⊢ (F^{-1} Fn P \land F [t] \subseteq P \land v \in F [t]) \to F^{-1} (v) \in F^{-1} [F [t]]$
214	199 211 212 213	syl3anc	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F^{-1} (v) \in F^{-1} [F [t]]$
215	205	simprd	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to t \in 𝒫 B$
216	215	elpwid	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to t \subseteq B$
217		f1imacnv	$⊢ (F : B \underset{1-1}{⟶} P \land t \subseteq B) \to F^{-1} [F [t]] = t$
218	204 216 217	syl2anc	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F^{-1} [F [t]] = t$
219	214 218	eleqtrd	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F^{-1} (v) \in t$
220		simpllr	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to \forall x \in s \forall y \in t x \in (a J y)$
221		eleq1	$⊢ x = F^{-1} (u) \to (x \in (a J y) \leftrightarrow F^{-1} (u) \in (a J y))$
222		oveq2	$⊢ y = F^{-1} (v) \to a J y = a J F^{-1} (v)$
223	222	eleq2d	$⊢ y = F^{-1} (v) \to (F^{-1} (u) \in (a J y) \leftrightarrow F^{-1} (u) \in (a J F^{-1} (v)))$
224	221 223	rspc2va	$⊢ ((F^{-1} (u) \in s \land F^{-1} (v) \in t) \land \forall x \in s \forall y \in t x \in (a J y)) \to F^{-1} (u) \in (a J F^{-1} (v))$
225	210 219 220 224	syl21anc	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F^{-1} (u) \in (a J F^{-1} (v))$
226		simp-6l	$⊢ ((((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \land (e \in B \land f \in B)) \to φ$
227	226 8	sylancom	$⊢ ((((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \land (e \in B \land f \in B)) \to e E f = F (e) D F (f)$
228		simp-6l	$⊢ ((((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \land (e \in B \land f \in B \land g \in B)) \to φ$
229	228 9	sylancom	$⊢ ((((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \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)))$
230		simp-4r	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to a \in B$
231	211 212	sseldd	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to v \in P$
232		f1ocnvdm	$⊢ (F : B \underset{1-1 onto}{⟶} P \land v \in P) \to F^{-1} (v) \in B$
233	197 231 232	syl2anc	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F^{-1} (v) \in B$
234	200 201	sseldd	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to u \in P$
235		f1ocnvdm	$⊢ (F : B \underset{1-1 onto}{⟶} P \land u \in P) \to F^{-1} (u) \in B$
236	197 234 235	syl2anc	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F^{-1} (u) \in B$
237	1 2 3 4 5 6 197 227 229 230 233 236	f1otrgitv	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to (F^{-1} (u) \in (a J F^{-1} (v)) \leftrightarrow F (F^{-1} (u)) \in (F (a) I F (F^{-1} (v))))$
238	225 237	mpbid	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F (F^{-1} (u)) \in (F (a) I F (F^{-1} (v)))$
239		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} P \land u \in P) \to F (F^{-1} (u)) = u$
240	197 234 239	syl2anc	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F (F^{-1} (u)) = u$
241		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} P \land v \in P) \to F (F^{-1} (v)) = v$
242	197 231 241	syl2anc	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F (F^{-1} (v)) = v$
243	242	oveq2d	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to F (a) I F (F^{-1} (v)) = F (a) I v$
244	238 240 243	3eltr3d	$⊢ (((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s]) \land v \in F [t]) \to u \in (F (a) I v)$
245	244	3impa	$⊢ ((((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \land u \in F [s] \land v \in F [t]) \to u \in (F (a) I v)$
246	1 2 3 185 191 193 196 245	axtgcont	$⊢ (((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \to \exists c \in P \forall e \in F [s] \forall f \in F [t] c \in (e I f)$
247	184 246	r19.29a	$⊢ (((φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \land a \in B) \land \forall x \in s \forall y \in t x \in (a J y)) \to \exists b \in B \forall x \in s \forall y \in t b \in (x J y)$
248	247	rexlimdva2	$⊢ (φ \land (s \in 𝒫 B \land t \in 𝒫 B)) \to (\exists a \in B \forall x \in s \forall y \in t x \in (a J y) \to \exists b \in B \forall x \in s \forall y \in t b \in (x J y))$
249	248	ralrimivva	$⊢ φ \to \forall s \in 𝒫 B \forall t \in 𝒫 B (\exists a \in B \forall x \in s \forall y \in t x \in (a J y) \to \exists b \in B \forall x \in s \forall y \in t b \in (x J y))$
250	74 132 249	3jca	$⊢ φ \to (\forall x \in B \forall y \in B (y \in (x J x) \to x = y) \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 z) \land v \in (y J z)) \to \exists a \in B (a \in (u J y) \land a \in (v J x))) \land \forall s \in 𝒫 B \forall t \in 𝒫 B (\exists a \in B \forall x \in s \forall y \in t x \in (a J y) \to \exists b \in B \forall x \in s \forall y \in t b \in (x J y)))$
251	4 5 6	istrkgb	$⊢ H \in 𝒢_{Tarski}^{B} \leftrightarrow (H \in V \land (\forall x \in B \forall y \in B (y \in (x J x) \to x = y) \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 z) \land v \in (y J z)) \to \exists a \in B (a \in (u J y) \land a \in (v J x))) \land \forall s \in 𝒫 B \forall t \in 𝒫 B (\exists a \in B \forall x \in s \forall y \in t x \in (a J y) \to \exists b \in B \forall x \in s \forall y \in t b \in (x J y))))$
252	13 250 251	sylanbrc	$⊢ φ \to H \in 𝒢_{Tarski}^{B}$
253	57 252	elind	$⊢ φ \to H \in (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B})$
254	11	ad9antr	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to G \in 𝒢_{Tarski}$
255	16	ad9antr	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F : B ⟶ P$
256		simp-9r	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to x \in B$
257	255 256	ffvelrnd	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (x) \in P$
258		simp-8r	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to y \in B$
259	255 258	ffvelrnd	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (y) \in P$
260		simp-7r	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to z \in B$
261	255 260	ffvelrnd	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (z) \in P$
262		simp-5r	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to a \in B$
263	255 262	ffvelrnd	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (a) \in P$
264		simp-4r	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to b \in B$
265	255 264	ffvelrnd	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (b) \in P$
266		simpllr	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to c \in B$
267	255 266	ffvelrnd	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (c) \in P$
268		simp-6r	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to u \in B$
269	255 268	ffvelrnd	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (u) \in P$
270		simplr	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to v \in B$
271	255 270	ffvelrnd	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (v) \in P$
272	7	ad9antr	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F : B \underset{1-1 onto}{⟶} P$
273	272 256	jca	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to (F : B \underset{1-1 onto}{⟶} P \land x \in B)$
274		simprl1	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to x \neq y$
275		dff1o6	$⊢ F : B \underset{1-1 onto}{⟶} P \leftrightarrow (F Fn B \land ran F = P \land \forall x \in B \forall y \in B (F (x) = F (y) \to x = y))$
276	275	simp3bi	$⊢ F : B \underset{1-1 onto}{⟶} P \to \forall x \in B \forall y \in B (F (x) = F (y) \to x = y)$
277	276	r19.21bi	$⊢ (F : B \underset{1-1 onto}{⟶} P \land x \in B) \to \forall y \in B (F (x) = F (y) \to x = y)$
278	277	r19.21bi	$⊢ ((F : B \underset{1-1 onto}{⟶} P \land x \in B) \land y \in B) \to (F (x) = F (y) \to x = y)$
279	278	necon3d	$⊢ ((F : B \underset{1-1 onto}{⟶} P \land x \in B) \land y \in B) \to (x \neq y \to F (x) \neq F (y))$
280	279	imp	$⊢ (((F : B \underset{1-1 onto}{⟶} P \land x \in B) \land y \in B) \land x \neq y) \to F (x) \neq F (y)$
281	273 258 274 280	syl21anc	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (x) \neq F (y)$
282		simprl2	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to y \in (x J z)$
283	8	ex	$⊢ φ \to ((e \in B \land f \in B) \to e E f = F (e) D F (f))$
284	283	ad9antr	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to ((e \in B \land f \in B) \to e E f = F (e) D F (f))$
285	284	imp	$⊢ ((((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \land (e \in B \land f \in B)) \to e E f = F (e) D F (f)$
286	9	ex	$⊢ φ \to ((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))))$
287	286	ad9antr	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to ((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))))$
288	287	imp	$⊢ ((((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \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)))$
289	1 2 3 4 5 6 272 285 288 256 260 258	f1otrgitv	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to (y \in (x J z) \leftrightarrow F (y) \in (F (x) I F (z)))$
290	282 289	mpbid	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (y) \in (F (x) I F (z))$
291		simprl3	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to b \in (a J c)$
292	1 2 3 4 5 6 272 285 288 262 266 264	f1otrgitv	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to (b \in (a J c) \leftrightarrow F (b) \in (F (a) I F (c)))$
293	291 292	mpbid	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (b) \in (F (a) I F (c))$
294		simprr	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v))$
295	294	simpld	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to (x E y = a E b \land y E z = b E c)$
296	295	simpld	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to x E y = a E b$
297	1 2 3 4 5 6 272 285 288 256 258	f1otrgds	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to x E y = F (x) D F (y)$
298	1 2 3 4 5 6 272 285 288 262 264	f1otrgds	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to a E b = F (a) D F (b)$
299	296 297 298	3eqtr3d	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (x) D F (y) = F (a) D F (b)$
300	295	simprd	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to y E z = b E c$
301	1 2 3 4 5 6 272 285 288 258 260	f1otrgds	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to y E z = F (y) D F (z)$
302	1 2 3 4 5 6 272 285 288 264 266	f1otrgds	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to b E c = F (b) D F (c)$
303	300 301 302	3eqtr3d	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (y) D F (z) = F (b) D F (c)$
304	294	simprd	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to (x E u = a E v \land y E u = b E v)$
305	304	simpld	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to x E u = a E v$
306	1 2 3 4 5 6 272 285 288 256 268	f1otrgds	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to x E u = F (x) D F (u)$
307	1 2 3 4 5 6 272 285 288 262 270	f1otrgds	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to a E v = F (a) D F (v)$
308	305 306 307	3eqtr3d	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (x) D F (u) = F (a) D F (v)$
309	304	simprd	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to y E u = b E v$
310	1 2 3 4 5 6 272 285 288 258 268	f1otrgds	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to y E u = F (y) D F (u)$
311	1 2 3 4 5 6 272 285 288 264 270	f1otrgds	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to b E v = F (b) D F (v)$
312	309 310 311	3eqtr3d	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (y) D F (u) = F (b) D F (v)$
313	1 2 3 254 257 259 261 263 265 267 269 271 281 290 293 299 303 308 312	axtg5seg	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to F (z) D F (u) = F (c) D F (v)$
314	1 2 3 4 5 6 272 285 288 260 268	f1otrgds	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to z E u = F (z) D F (u)$
315	1 2 3 4 5 6 272 285 288 266 270	f1otrgds	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to c E v = F (c) D F (v)$
316	313 314 315	3eqtr4d	$⊢ (((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \land ((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v)))) \to z E u = c E v$
317	316	ex	$⊢ ((((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \land v \in B) \to (((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v))) \to z E u = c E v)$
318	317	ralrimiva	$⊢ (((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \land c \in B) \to \forall v \in B (((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v))) \to z E u = c E v)$
319	318	ralrimiva	$⊢ ((((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \land b \in B) \to \forall c \in B \forall v \in B (((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v))) \to z E u = c E v)$
320	319	ralrimiva	$⊢ (((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \land a \in B) \to \forall b \in B \forall c \in B \forall v \in B (((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v))) \to z E u = c E v)$
321	320	ralrimiva	$⊢ ((((φ \land x \in B) \land y \in B) \land z \in B) \land u \in B) \to \forall a \in B \forall b \in B \forall c \in B \forall v \in B (((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v))) \to z E u = c E v)$
322	321	ralrimiva	$⊢ (((φ \land x \in B) \land y \in B) \land z \in B) \to \forall u \in B \forall a \in B \forall b \in B \forall c \in B \forall v \in B (((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v))) \to z E u = c E v)$
323	322	ralrimiva	$⊢ ((φ \land x \in B) \land y \in B) \to \forall z \in B \forall u \in B \forall a \in B \forall b \in B \forall c \in B \forall v \in B (((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v))) \to z E u = c E v)$
324	323	ralrimiva	$⊢ (φ \land x \in B) \to \forall y \in B \forall z \in B \forall u \in B \forall a \in B \forall b \in B \forall c \in B \forall v \in B (((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v))) \to z E u = c E v)$
325	324	ralrimiva	$⊢ φ \to \forall x \in B \forall y \in B \forall z \in B \forall u \in B \forall a \in B \forall b \in B \forall c \in B \forall v \in B (((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v))) \to z E u = c E v)$
326		simp-4l	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to φ$
327		simplr	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to w \in P$
328		simprl	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to F (y) \in (F (x) I w)$
329	326 7	syl	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to F : B \underset{1-1 onto}{⟶} P$
330		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} P \land w \in P) \to F (F^{-1} (w)) = w$
331	329 327 330	syl2anc	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to F (F^{-1} (w)) = w$
332	331	oveq2d	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to F (x) I F (F^{-1} (w)) = F (x) I w$
333	328 332	eleqtrrd	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to F (y) \in (F (x) I F (F^{-1} (w)))$
334	326 8	sylan	$⊢ (((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \land (e \in B \land f \in B)) \to e E f = F (e) D F (f)$
335	326 9	sylan	$⊢ (((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \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)))$
336	18	ad3antrrr	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to x \in B$
337	77	ffvelrnda	$⊢ (φ \land w \in P) \to F^{-1} (w) \in B$
338	326 327 337	syl2anc	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to F^{-1} (w) \in B$
339	20	ad3antrrr	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to y \in B$
340	1 2 3 4 5 6 329 334 335 336 338 339	f1otrgitv	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to (y \in (x J F^{-1} (w)) \leftrightarrow F (y) \in (F (x) I F (F^{-1} (w))))$
341	333 340	mpbird	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to y \in (x J F^{-1} (w))$
342	1 2 3 4 5 6 329 334 335 339 338	f1otrgds	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to y E F^{-1} (w) = F (y) D F (F^{-1} (w))$
343	331	oveq2d	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to F (y) D F (F^{-1} (w)) = F (y) D w$
344		simprr	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to F (y) D w = F (a) D F (b)$
345	342 343 344	3eqtrd	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to y E F^{-1} (w) = F (a) D F (b)$
346		simprl	$⊢ ((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \to a \in B$
347	346	ad2antrr	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to a \in B$
348		simprr	$⊢ ((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \to b \in B$
349	348	ad2antrr	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to b \in B$
350	1 2 3 4 5 6 329 334 335 347 349	f1otrgds	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to a E b = F (a) D F (b)$
351	345 350	eqtr4d	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to y E F^{-1} (w) = a E b$
352		oveq2	$⊢ z = F^{-1} (w) \to x J z = x J F^{-1} (w)$
353	352	eleq2d	$⊢ z = F^{-1} (w) \to (y \in (x J z) \leftrightarrow y \in (x J F^{-1} (w)))$
354		oveq2	$⊢ z = F^{-1} (w) \to y E z = y E F^{-1} (w)$
355	354	eqeq1d	$⊢ z = F^{-1} (w) \to (y E z = a E b \leftrightarrow y E F^{-1} (w) = a E b)$
356	353 355	anbi12d	$⊢ z = F^{-1} (w) \to ((y \in (x J z) \land y E z = a E b) \leftrightarrow (y \in (x J F^{-1} (w)) \land y E F^{-1} (w) = a E b))$
357	356	adantl	$⊢ ((φ \land w \in P) \land z = F^{-1} (w)) \to ((y \in (x J z) \land y E z = a E b) \leftrightarrow (y \in (x J F^{-1} (w)) \land y E F^{-1} (w) = a E b))$
358	337 357	rspcedv	$⊢ (φ \land w \in P) \to ((y \in (x J F^{-1} (w)) \land y E F^{-1} (w) = a E b) \to \exists z \in B (y \in (x J z) \land y E z = a E b))$
359	358	imp	$⊢ ((φ \land w \in P) \land (y \in (x J F^{-1} (w)) \land y E F^{-1} (w) = a E b)) \to \exists z \in B (y \in (x J z) \land y E z = a E b)$
360	326 327 341 351 359	syl22anc	$⊢ ((((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \land w \in P) \land (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))) \to \exists z \in B (y \in (x J z) \land y E z = a E b)$
361	14	adantr	$⊢ ((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \to G \in 𝒢_{Tarski}$
362	19	adantr	$⊢ ((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \to F (x) \in P$
363	21	adantr	$⊢ ((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \to F (y) \in P$
364	17	adantr	$⊢ ((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \to F : B ⟶ P$
365	364 346	ffvelrnd	$⊢ ((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \to F (a) \in P$
366	364 348	ffvelrnd	$⊢ ((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \to F (b) \in P$
367	1 2 3 361 362 363 365 366	axtgsegcon	$⊢ ((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \to \exists w \in P (F (y) \in (F (x) I w) \land F (y) D w = F (a) D F (b))$
368	360 367	r19.29a	$⊢ ((φ \land (x \in B \land y \in B)) \land (a \in B \land b \in B)) \to \exists z \in B (y \in (x J z) \land y E z = a E b)$
369	368	ralrimivva	$⊢ (φ \land (x \in B \land y \in B)) \to \forall a \in B \forall b \in B \exists z \in B (y \in (x J z) \land y E z = a E b)$
370	369	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B \forall a \in B \forall b \in B \exists z \in B (y \in (x J z) \land y E z = a E b)$
371	13 325 370	jca32	$⊢ φ \to (H \in V \land (\forall x \in B \forall y \in B \forall z \in B \forall u \in B \forall a \in B \forall b \in B \forall c \in B \forall v \in B (((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v))) \to z E u = c E v) \land \forall x \in B \forall y \in B \forall a \in B \forall b \in B \exists z \in B (y \in (x J z) \land y E z = a E b)))$
372	4 5 6	istrkgcb	$⊢ H \in 𝒢_{Tarski}^{CB} \leftrightarrow (H \in V \land (\forall x \in B \forall y \in B \forall z \in B \forall u \in B \forall a \in B \forall b \in B \forall c \in B \forall v \in B (((x \neq y \land y \in (x J z) \land b \in (a J c)) \land ((x E y = a E b \land y E z = b E c) \land (x E u = a E v \land y E u = b E v))) \to z E u = c E v) \land \forall x \in B \forall y \in B \forall a \in B \forall b \in B \exists z \in B (y \in (x J z) \land y E z = a E b)))$
373	371 372	sylibr	$⊢ φ \to H \in 𝒢_{Tarski}^{CB}$
374	4 5 6	istrkgl	$⊢ H \in \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\} \leftrightarrow (H \in V \land {Line}_{𝒢} (H) = (x \in B, y \in (B ∖ \{x\}) ⟼ \{z \in B \| (z \in (x J y) \lor x \in (z J y) \lor y \in (x J z))\}))$
375	13 12 374	sylanbrc	$⊢ φ \to H \in \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}$
376	373 375	elind	$⊢ φ \to H \in (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\})$
377	253 376	elind	$⊢ φ \to H \in ((𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}))$
378		df-trkg	$⊢ 𝒢_{Tarski} = (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\})$
379	377 378	eleqtrrdi	$⊢ φ \to H \in 𝒢_{Tarski}$

Metamath Proof Explorer

Theorem f1otrg

Proof