Theorem 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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	f1otrkg.d	⊢ 𝐷 = ( dist ‘ 𝐺 )
	f1otrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	f1otrkg.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
	f1otrkg.e	⊢ 𝐸 = ( dist ‘ 𝐻 )
	f1otrkg.j	⊢ 𝐽 = ( Itv ‘ 𝐻 )
	f1otrkg.f	⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝑃 )
	f1otrkg.1	⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) → ( 𝑒 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑒 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) )
	f1otrkg.2	⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑔 ∈ ( 𝑒 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) )
	f1otrg.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑉 )
	f1otrge.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
Assertion	f1otrge	⊢ ( 𝜑 → 𝐻 ∈ TarskiGE )

Proof

Step	Hyp	Ref	Expression
1		f1otrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		f1otrkg.d	⊢ 𝐷 = ( dist ‘ 𝐺 )
3		f1otrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		f1otrkg.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
5		f1otrkg.e	⊢ 𝐸 = ( dist ‘ 𝐻 )
6		f1otrkg.j	⊢ 𝐽 = ( Itv ‘ 𝐻 )
7		f1otrkg.f	⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝑃 )
8		f1otrkg.1	⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) → ( 𝑒 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑒 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) )
9		f1otrkg.2	⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑔 ∈ ( 𝑒 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) )
10		f1otrg.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑉 )
11		f1otrge.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
12	10	elexd	⊢ ( 𝜑 → 𝐻 ∈ V )
13		f1ocnv	⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 → ◡ 𝐹 : 𝑃 –1-1-onto→ 𝐵 )
14		f1of	⊢ ( ◡ 𝐹 : 𝑃 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝑃 ⟶ 𝐵 )
15	7 13 14	3syl	⊢ ( 𝜑 → ◡ 𝐹 : 𝑃 ⟶ 𝐵 )
16	15	ad6antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ◡ 𝐹 : 𝑃 ⟶ 𝐵 )
17		simpllr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → 𝑐 ∈ 𝑃 )
18	16 17	ffvelrnd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( ◡ 𝐹 ‘ 𝑐 ) ∈ 𝐵 )
19		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → 𝑑 ∈ 𝑃 )
20	16 19	ffvelrnd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( ◡ 𝐹 ‘ 𝑑 ) ∈ 𝐵 )
21		simpr1	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) )
22	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝑃 )
23	22	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝑃 )
24		f1ocnvfv2	⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 ∧ 𝑐 ∈ 𝑃 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑐 ) ) = 𝑐 )
25	23 17 24	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑐 ) ) = 𝑐 )
26	25	oveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐼 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑐 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) )
27	21 26	eleqtrrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑐 ) ) ) )
28	8	ad5ant15	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) → ( 𝑒 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑒 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) )
29	28	ad5ant15	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) → ( 𝑒 𝐸 𝑓 ) = ( ( 𝐹 ‘ 𝑒 ) 𝐷 ( 𝐹 ‘ 𝑓 ) ) )
30	9	ad5ant15	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑔 ∈ ( 𝑒 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) )
31	30	ad5ant15	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) ∧ ( 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑔 ∈ ( 𝑒 𝐽 𝑓 ) ↔ ( 𝐹 ‘ 𝑔 ) ∈ ( ( 𝐹 ‘ 𝑒 ) 𝐼 ( 𝐹 ‘ 𝑓 ) ) ) )
32		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
33	32	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → 𝑥 ∈ 𝐵 )
34	33	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → 𝑥 ∈ 𝐵 )
35		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
36	35	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → 𝑦 ∈ 𝐵 )
37	36	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → 𝑦 ∈ 𝐵 )
38	1 2 3 4 5 6 23 29 31 34 18 37	f1otrgitv	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( 𝑦 ∈ ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑐 ) ) ↔ ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑐 ) ) ) ) )
39	27 38	mpbird	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → 𝑦 ∈ ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑐 ) ) )
40		simpr2	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) )
41		f1ocnvfv2	⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 ∧ 𝑑 ∈ 𝑃 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑑 ) ) = 𝑑 )
42	23 19 41	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑑 ) ) = 𝑑 )
43	42	oveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐼 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑑 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) )
44	40 43	eleqtrrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑑 ) ) ) )
45		simplr1	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → 𝑧 ∈ 𝐵 )
46	45	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → 𝑧 ∈ 𝐵 )
47	1 2 3 4 5 6 23 29 31 34 20 46	f1otrgitv	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( 𝑧 ∈ ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑑 ) ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑑 ) ) ) ) )
48	44 47	mpbird	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → 𝑧 ∈ ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑑 ) ) )
49		simpr3	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) )
50	25 42	oveq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑐 ) ) 𝐼 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑑 ) ) ) = ( 𝑐 𝐼 𝑑 ) )
51	49 50	eleqtrrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( 𝐹 ‘ 𝑣 ) ∈ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑐 ) ) 𝐼 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑑 ) ) ) )
52		simplr3	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → 𝑣 ∈ 𝐵 )
53	52	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → 𝑣 ∈ 𝐵 )
54	1 2 3 4 5 6 23 29 31 18 20 53	f1otrgitv	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ( 𝑣 ∈ ( ( ◡ 𝐹 ‘ 𝑐 ) 𝐽 ( ◡ 𝐹 ‘ 𝑑 ) ) ↔ ( 𝐹 ‘ 𝑣 ) ∈ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑐 ) ) 𝐼 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑑 ) ) ) ) )
55	51 54	mpbird	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → 𝑣 ∈ ( ( ◡ 𝐹 ‘ 𝑐 ) 𝐽 ( ◡ 𝐹 ‘ 𝑑 ) ) )
56		oveq2	⊢ ( 𝑎 = ( ◡ 𝐹 ‘ 𝑐 ) → ( 𝑥 𝐽 𝑎 ) = ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑐 ) ) )
57	56	eleq2d	⊢ ( 𝑎 = ( ◡ 𝐹 ‘ 𝑐 ) → ( 𝑦 ∈ ( 𝑥 𝐽 𝑎 ) ↔ 𝑦 ∈ ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑐 ) ) ) )
58		oveq1	⊢ ( 𝑎 = ( ◡ 𝐹 ‘ 𝑐 ) → ( 𝑎 𝐽 𝑏 ) = ( ( ◡ 𝐹 ‘ 𝑐 ) 𝐽 𝑏 ) )
59	58	eleq2d	⊢ ( 𝑎 = ( ◡ 𝐹 ‘ 𝑐 ) → ( 𝑣 ∈ ( 𝑎 𝐽 𝑏 ) ↔ 𝑣 ∈ ( ( ◡ 𝐹 ‘ 𝑐 ) 𝐽 𝑏 ) ) )
60	57 59	3anbi13d	⊢ ( 𝑎 = ( ◡ 𝐹 ‘ 𝑐 ) → ( ( 𝑦 ∈ ( 𝑥 𝐽 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐽 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐽 𝑏 ) ) ↔ ( 𝑦 ∈ ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑐 ) ) ∧ 𝑧 ∈ ( 𝑥 𝐽 𝑏 ) ∧ 𝑣 ∈ ( ( ◡ 𝐹 ‘ 𝑐 ) 𝐽 𝑏 ) ) ) )
61		oveq2	⊢ ( 𝑏 = ( ◡ 𝐹 ‘ 𝑑 ) → ( 𝑥 𝐽 𝑏 ) = ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑑 ) ) )
62	61	eleq2d	⊢ ( 𝑏 = ( ◡ 𝐹 ‘ 𝑑 ) → ( 𝑧 ∈ ( 𝑥 𝐽 𝑏 ) ↔ 𝑧 ∈ ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑑 ) ) ) )
63		oveq2	⊢ ( 𝑏 = ( ◡ 𝐹 ‘ 𝑑 ) → ( ( ◡ 𝐹 ‘ 𝑐 ) 𝐽 𝑏 ) = ( ( ◡ 𝐹 ‘ 𝑐 ) 𝐽 ( ◡ 𝐹 ‘ 𝑑 ) ) )
64	63	eleq2d	⊢ ( 𝑏 = ( ◡ 𝐹 ‘ 𝑑 ) → ( 𝑣 ∈ ( ( ◡ 𝐹 ‘ 𝑐 ) 𝐽 𝑏 ) ↔ 𝑣 ∈ ( ( ◡ 𝐹 ‘ 𝑐 ) 𝐽 ( ◡ 𝐹 ‘ 𝑑 ) ) ) )
65	62 64	3anbi23d	⊢ ( 𝑏 = ( ◡ 𝐹 ‘ 𝑑 ) → ( ( 𝑦 ∈ ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑐 ) ) ∧ 𝑧 ∈ ( 𝑥 𝐽 𝑏 ) ∧ 𝑣 ∈ ( ( ◡ 𝐹 ‘ 𝑐 ) 𝐽 𝑏 ) ) ↔ ( 𝑦 ∈ ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑐 ) ) ∧ 𝑧 ∈ ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑑 ) ) ∧ 𝑣 ∈ ( ( ◡ 𝐹 ‘ 𝑐 ) 𝐽 ( ◡ 𝐹 ‘ 𝑑 ) ) ) ) )
66	60 65	rspc2ev	⊢ ( ( ( ◡ 𝐹 ‘ 𝑐 ) ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ 𝑑 ) ∈ 𝐵 ∧ ( 𝑦 ∈ ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑐 ) ) ∧ 𝑧 ∈ ( 𝑥 𝐽 ( ◡ 𝐹 ‘ 𝑑 ) ) ∧ 𝑣 ∈ ( ( ◡ 𝐹 ‘ 𝑐 ) 𝐽 ( ◡ 𝐹 ‘ 𝑑 ) ) ) ) → ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝐵 ( 𝑦 ∈ ( 𝑥 𝐽 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐽 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐽 𝑏 ) ) )
67	18 20 39 48 55 66	syl113anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) ) → ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝐵 ( 𝑦 ∈ ( 𝑥 𝐽 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐽 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐽 𝑏 ) ) )
68	11	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → 𝐺 ∈ TarskiGE )
69		f1of	⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 → 𝐹 : 𝐵 ⟶ 𝑃 )
70	7 69	syl	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝑃 )
71	70	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐹 : 𝐵 ⟶ 𝑃 )
72	71 32	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑃 )
73	72	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑃 )
74	71 35	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑃 )
75	74	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑃 )
76	70	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → 𝐹 : 𝐵 ⟶ 𝑃 )
77	76 45	ffvelrnd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑃 )
78		simplr2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → 𝑢 ∈ 𝐵 )
79	76 78	ffvelrnd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → ( 𝐹 ‘ 𝑢 ) ∈ 𝑃 )
80	76 52	ffvelrnd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝑃 )
81		simpr1	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) )
82	1 2 3 4 5 6 22 28 30 33 52 78	f1otrgitv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ↔ ( 𝐹 ‘ 𝑢 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 ( 𝐹 ‘ 𝑣 ) ) ) )
83	81 82	mpbid	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → ( 𝐹 ‘ 𝑢 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 ( 𝐹 ‘ 𝑣 ) ) )
84		simpr2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) )
85	1 2 3 4 5 6 22 28 30 36 45 78	f1otrgitv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → ( 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ↔ ( 𝐹 ‘ 𝑢 ) ∈ ( ( 𝐹 ‘ 𝑦 ) 𝐼 ( 𝐹 ‘ 𝑧 ) ) ) )
86	84 85	mpbid	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → ( 𝐹 ‘ 𝑢 ) ∈ ( ( 𝐹 ‘ 𝑦 ) 𝐼 ( 𝐹 ‘ 𝑧 ) ) )
87		simpr3	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → 𝑥 ≠ 𝑢 )
88		dff1o6	⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 ↔ ( 𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑢 ) → 𝑥 = 𝑢 ) ) )
89	88	simp3bi	⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑢 ) → 𝑥 = 𝑢 ) )
90	89	r19.21bi	⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑢 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑢 ) → 𝑥 = 𝑢 ) )
91	90	r19.21bi	⊢ ( ( ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑢 ) → 𝑥 = 𝑢 ) )
92	91	necon3d	⊢ ( ( ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑥 ≠ 𝑢 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑢 ) ) )
93	92	imp	⊢ ( ( ( ( 𝐹 : 𝐵 –1-1-onto→ 𝑃 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑢 ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑢 ) )
94	22 33 78 87 93	syl1111anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑢 ) )
95	1 2 3 68 73 75 77 79 80 83 86 94	axtgeucl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑐 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐼 𝑑 ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝑐 𝐼 𝑑 ) ) )
96	67 95	r19.29vva	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) → ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝐵 ( 𝑦 ∈ ( 𝑥 𝐽 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐽 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐽 𝑏 ) ) )
97	96	ex	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝐵 ( 𝑦 ∈ ( 𝑥 𝐽 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐽 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐽 𝑏 ) ) ) )
98	97	ralrimivvva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝐵 ( 𝑦 ∈ ( 𝑥 𝐽 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐽 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐽 𝑏 ) ) ) )
99	98	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝐵 ( 𝑦 ∈ ( 𝑥 𝐽 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐽 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐽 𝑏 ) ) ) )
100	4 5 6	istrkge	⊢ ( 𝐻 ∈ TarskiGE ↔ ( 𝐻 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 ∈ ( 𝑥 𝐽 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝐵 ( 𝑦 ∈ ( 𝑥 𝐽 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐽 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐽 𝑏 ) ) ) ) )
101	12 99 100	sylanbrc	⊢ ( 𝜑 → 𝐻 ∈ TarskiGE )