Metamath Proof Explorer


Theorem 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 𝑃 = ( 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 ( 𝜑𝐻𝑉 )
f1otrg.g ( 𝜑𝐺 ∈ TarskiG )
f1otrg.l ( 𝜑 → ( LineG ‘ 𝐻 ) = ( 𝑥𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑧𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐽 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐽 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐽 𝑧 ) ) } ) )
Assertion f1otrg ( 𝜑𝐻 ∈ TarskiG )

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