MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1otrg Structured version   Visualization version   GIF version
Theorem f1otrg 28695
Description: A bijection between bases which conserves distances and intervals conserves also geometries. (Contributed by Thierry Arnoux, 23-Mar-2019.)
Hypotheses
Ref Expression
f1otrkg.p 𝑃 = (Baseβ€˜πΊ)
f1otrkg.d 𝐷 = (distβ€˜πΊ)
f1otrkg.i 𝐼 = (Itvβ€˜πΊ)
f1otrkg.b 𝐡 = (Baseβ€˜π»)
f1otrkg.e 𝐸 = (distβ€˜π»)
f1otrkg.j 𝐽 = (Itvβ€˜π»)
f1otrkg.f (πœ‘ β†’ 𝐹:𝐡–1-1-onto→𝑃)
f1otrkg.1 ((πœ‘ ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
f1otrkg.2 ((πœ‘ ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
f1otrg.h (πœ‘ β†’ 𝐻 ∈ 𝑉)
f1otrg.g (πœ‘ β†’ 𝐺 ∈ TarskiG)
f1otrg.l (πœ‘ β†’ (LineGβ€˜π») = (π‘₯ ∈ 𝐡, 𝑦 ∈ (𝐡 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝐡 ∣ (𝑧 ∈ (π‘₯𝐽𝑦) ∨ π‘₯ ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (π‘₯𝐽𝑧))}))
Assertion
Ref Expression
f1otrg (πœ‘ β†’ 𝐻 ∈ TarskiG)
Distinct variable groups:   𝑒,𝑓,𝑔,π‘₯,𝑦,𝑧,𝐡   𝐷,𝑒,𝑓,𝑔   𝑒,𝐸,𝑓,𝑔,π‘₯,𝑦,𝑧   𝑒,𝐹,𝑓,𝑔,π‘₯,𝑦,𝑧   𝑒,𝐼,𝑓,𝑔,π‘₯,𝑦   𝑒,𝐽,𝑓,𝑔,π‘₯,𝑦,𝑧   𝑃,𝑒,𝑓,𝑔,π‘₯,𝑦,𝑧   πœ‘,𝑒,𝑓,𝑔,π‘₯,𝑦,𝑧   𝑓,𝐻
Allowed substitution hints:   𝐷(π‘₯,𝑦,𝑧)   𝐺(π‘₯,𝑦,𝑧,𝑒,𝑓,𝑔)   𝐻(π‘₯,𝑦,𝑧,𝑒,𝑔)   𝐼(𝑧)   𝑉(π‘₯,𝑦,𝑧,𝑒,𝑓,𝑔)
Proof of Theorem f1otrg
Dummy variables π‘Ž 𝑏 𝑐 𝑖 𝑝 𝑠 𝑑 𝑒 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1otrg.h . . . . . 6 (πœ‘ β†’ 𝐻 ∈ 𝑉)
21elexd 3494 . . . . 5 (πœ‘ β†’ 𝐻 ∈ V)
3 f1otrkg.p . . . . . . . . 9 𝑃 = (Baseβ€˜πΊ)
4 f1otrkg.d . . . . . . . . 9 𝐷 = (distβ€˜πΊ)
5 f1otrkg.i . . . . . . . . 9 𝐼 = (Itvβ€˜πΊ)
6 f1otrg.g . . . . . . . . . 10 (πœ‘ β†’ 𝐺 ∈ TarskiG)
76adantr 479 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ 𝐺 ∈ TarskiG)
8 f1otrkg.f . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹:𝐡–1-1-onto→𝑃)
9 f1of 6844 . . . . . . . . . . . 12 (𝐹:𝐡–1-1-onto→𝑃 β†’ 𝐹:π΅βŸΆπ‘ƒ)
108, 9syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹:π΅βŸΆπ‘ƒ)
1110adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
12 simprl 769 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ π‘₯ ∈ 𝐡)
1311, 12ffvelcdmd 7100 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
14 simprr 771 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ 𝑦 ∈ 𝐡)
1511, 14ffvelcdmd 7100 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
163, 4, 5, 7, 13, 15axtgcgrrflx 28286 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘₯)))
17 f1otrkg.b . . . . . . . . 9 𝐡 = (Baseβ€˜π»)
18 f1otrkg.e . . . . . . . . 9 𝐸 = (distβ€˜π»)
19 f1otrkg.j . . . . . . . . 9 𝐽 = (Itvβ€˜π»)
208adantr 479 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
21 f1otrkg.1 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
2221adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
23 f1otrkg.2 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
2423adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
253, 4, 5, 17, 18, 19, 20, 22, 24, 12, 14f1otrgds 28693 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (π‘₯𝐸𝑦) = ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)))
263, 4, 5, 17, 18, 19, 20, 22, 24, 14, 12f1otrgds 28693 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (𝑦𝐸π‘₯) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘₯)))
2716, 25, 263eqtr4d 2778 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (π‘₯𝐸𝑦) = (𝑦𝐸π‘₯))
2827ralrimivva 3198 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (π‘₯𝐸𝑦) = (𝑦𝐸π‘₯))
29 f1of1 6843 . . . . . . . . . . 11 (𝐹:𝐡–1-1-onto→𝑃 β†’ 𝐹:𝐡–1-1→𝑃)
308, 29syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:𝐡–1-1→𝑃)
31303ad2ant1 1130 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝐹:𝐡–1-1→𝑃)
32 simp21 1203 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ π‘₯ ∈ 𝐡)
33 simp22 1204 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝑦 ∈ 𝐡)
3432, 33jca 510 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡))
3563ad2ant1 1130 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝐺 ∈ TarskiG)
36103ad2ant1 1130 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
3736, 32ffvelcdmd 7100 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
3836, 33ffvelcdmd 7100 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
39 simp23 1205 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝑧 ∈ 𝐡)
4036, 39ffvelcdmd 7100 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (πΉβ€˜π‘§) ∈ 𝑃)
41 simp3 1135 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧))
4283ad2ant1 1130 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
43213ad2antl1 1182 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
44233ad2antl1 1182 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
453, 4, 5, 17, 18, 19, 42, 43, 44, 32, 33f1otrgds 28693 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (π‘₯𝐸𝑦) = ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)))
463, 4, 5, 17, 18, 19, 42, 43, 44, 39, 39f1otrgds 28693 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (𝑧𝐸𝑧) = ((πΉβ€˜π‘§)𝐷(πΉβ€˜π‘§)))
4741, 45, 463eqtr3d 2776 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)) = ((πΉβ€˜π‘§)𝐷(πΉβ€˜π‘§)))
483, 4, 5, 35, 37, 38, 40, 47axtgcgrid 28287 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘¦))
49 f1veqaeq 7273 . . . . . . . . . 10 ((𝐹:𝐡–1-1→𝑃 ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦))
5049imp 405 . . . . . . . . 9 (((𝐹:𝐡–1-1→𝑃 ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (πΉβ€˜π‘₯) = (πΉβ€˜π‘¦)) β†’ π‘₯ = 𝑦)
5131, 34, 48, 50syl21anc 836 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ π‘₯ = 𝑦)
52513expia 1118 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((π‘₯𝐸𝑦) = (𝑧𝐸𝑧) β†’ π‘₯ = 𝑦))
5352ralrimivvva 3201 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 ((π‘₯𝐸𝑦) = (𝑧𝐸𝑧) β†’ π‘₯ = 𝑦))
5428, 53jca 510 . . . . 5 (πœ‘ β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (π‘₯𝐸𝑦) = (𝑦𝐸π‘₯) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 ((π‘₯𝐸𝑦) = (𝑧𝐸𝑧) β†’ π‘₯ = 𝑦)))
5517, 18, 19istrkgc 28278 . . . . 5 (𝐻 ∈ TarskiGC ↔ (𝐻 ∈ V ∧ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (π‘₯𝐸𝑦) = (𝑦𝐸π‘₯) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 ((π‘₯𝐸𝑦) = (𝑧𝐸𝑧) β†’ π‘₯ = 𝑦))))
562, 54, 55sylanbrc 581 . . . 4 (πœ‘ β†’ 𝐻 ∈ TarskiGC)
5783ad2ant1 1130 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
5857, 29syl 17 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ 𝐹:𝐡–1-1→𝑃)
59 simp2 1134 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡))
6063ad2ant1 1130 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ 𝐺 ∈ TarskiG)
61133adant3 1129 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
62153adant3 1129 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
63 simp3 1135 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ 𝑦 ∈ (π‘₯𝐽π‘₯))
64213ad2antl1 1182 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
65233ad2antl1 1182 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
66123adant3 1129 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ π‘₯ ∈ 𝐡)
67143adant3 1129 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ 𝑦 ∈ 𝐡)
683, 4, 5, 17, 18, 19, 57, 64, 65, 66, 66, 67f1otrgitv 28694 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (𝑦 ∈ (π‘₯𝐽π‘₯) ↔ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘₯))))
6963, 68mpbid 231 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘₯)))
703, 4, 5, 60, 61, 62, 69axtgbtwnid 28290 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘¦))
7158, 59, 70, 50syl21anc 836 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ π‘₯ = 𝑦)
72713expia 1118 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (𝑦 ∈ (π‘₯𝐽π‘₯) β†’ π‘₯ = 𝑦))
7372ralrimivva 3198 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽π‘₯) β†’ π‘₯ = 𝑦))
74 f1ocnv 6856 . . . . . . . . . . . . . 14 (𝐹:𝐡–1-1-onto→𝑃 β†’ ◑𝐹:𝑃–1-1-onto→𝐡)
75 f1of 6844 . . . . . . . . . . . . . 14 (◑𝐹:𝑃–1-1-onto→𝐡 β†’ ◑𝐹:π‘ƒβŸΆπ΅)
768, 74, 753syl 18 . . . . . . . . . . . . 13 (πœ‘ β†’ ◑𝐹:π‘ƒβŸΆπ΅)
7776ad5antr 732 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ◑𝐹:π‘ƒβŸΆπ΅)
78 simplr 767 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑐 ∈ 𝑃)
7977, 78ffvelcdmd 7100 . . . . . . . . . . 11 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (β—‘πΉβ€˜π‘) ∈ 𝐡)
80 simpr 483 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ π‘Ž = (β—‘πΉβ€˜π‘)) β†’ π‘Ž = (β—‘πΉβ€˜π‘))
8180eleq1d 2814 . . . . . . . . . . . 12 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ π‘Ž = (β—‘πΉβ€˜π‘)) β†’ (π‘Ž ∈ (𝑒𝐽𝑦) ↔ (β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦)))
8280eleq1d 2814 . . . . . . . . . . . 12 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ π‘Ž = (β—‘πΉβ€˜π‘)) β†’ (π‘Ž ∈ (𝑣𝐽π‘₯) ↔ (β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯)))
8381, 82anbi12d 630 . . . . . . . . . . 11 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ π‘Ž = (β—‘πΉβ€˜π‘)) β†’ ((π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯)) ↔ ((β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦) ∧ (β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯))))
84 simprl 769 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)))
8520ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝐹:𝐡–1-1-onto→𝑃)
8685ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝐹:𝐡–1-1-onto→𝑃)
87 f1ocnvfv2 7292 . . . . . . . . . . . . . . . 16 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) = 𝑐)
8887eleq1d 2814 . . . . . . . . . . . . . . 15 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) β†’ ((πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ↔ 𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦))))
8986, 78, 88syl2anc 582 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ↔ 𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦))))
9084, 89mpbird 256 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)))
9122ad4ant14 750 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
9291ad4ant14 750 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
9324ad4ant14 750 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
9493ad4ant14 750 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
95 simplr2 1213 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑒 ∈ 𝐡)
9695ad2antrr 724 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑒 ∈ 𝐡)
9714ad2antrr 724 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑦 ∈ 𝐡)
9897ad2antrr 724 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑦 ∈ 𝐡)
993, 4, 5, 17, 18, 19, 86, 92, 94, 96, 98, 79f1otrgitv 28694 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦))))
10090, 99mpbird 256 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦))
101 simprr 771 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))
10287eleq1d 2814 . . . . . . . . . . . . . . 15 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) β†’ ((πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)) ↔ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯))))
10386, 78, 102syl2anc 582 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)) ↔ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯))))
104101, 103mpbird 256 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))
105 simplr3 1214 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑣 ∈ 𝐡)
106105ad2antrr 724 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑣 ∈ 𝐡)
10712ad2antrr 724 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ π‘₯ ∈ 𝐡)
108107ad2antrr 724 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ π‘₯ ∈ 𝐡)
1093, 4, 5, 17, 18, 19, 86, 92, 94, 106, 108, 79f1otrgitv 28694 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯))))
110104, 109mpbird 256 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯))
111100, 110jca 510 . . . . . . . . . . 11 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦) ∧ (β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯)))
11279, 83, 111rspcedvd 3613 . . . . . . . . . 10 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯)))
1137ad2antrr 724 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝐺 ∈ TarskiG)
11411ad2antrr 724 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝐹:π΅βŸΆπ‘ƒ)
115114, 107ffvelcdmd 7100 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
116114, 97ffvelcdmd 7100 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
117 simplr1 1212 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑧 ∈ 𝐡)
118114, 117ffvelcdmd 7100 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘§) ∈ 𝑃)
119114, 95ffvelcdmd 7100 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘’) ∈ 𝑃)
120114, 105ffvelcdmd 7100 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘£) ∈ 𝑃)
121 simprl 769 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑒 ∈ (π‘₯𝐽𝑧))
1223, 4, 5, 17, 18, 19, 85, 91, 93, 107, 117, 95f1otrgitv 28694 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (𝑒 ∈ (π‘₯𝐽𝑧) ↔ (πΉβ€˜π‘’) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘§))))
123121, 122mpbid 231 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘’) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘§)))
124 simprr 771 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑣 ∈ (𝑦𝐽𝑧))
1253, 4, 5, 17, 18, 19, 85, 91, 93, 97, 117, 105f1otrgitv 28694 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (𝑣 ∈ (𝑦𝐽𝑧) ↔ (πΉβ€˜π‘£) ∈ ((πΉβ€˜π‘¦)𝐼(πΉβ€˜π‘§))))
126124, 125mpbid 231 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘£) ∈ ((πΉβ€˜π‘¦)𝐼(πΉβ€˜π‘§)))
1273, 4, 5, 113, 115, 116, 118, 119, 120, 123, 126axtgpasch 28291 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ βˆƒπ‘ ∈ 𝑃 (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯))))
128112, 127r19.29a 3159 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯)))
129128ex 411 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) β†’ ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))))
130129ralrimivvva 3201 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))))
131130ralrimivva 3198 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))))
1328ad5antr 732 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
133 simpllr 774 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑐 ∈ 𝑃)
134132, 133, 87syl2anc 582 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) = 𝑐)
135 ffn 6727 . . . . . . . . . . . . . . . . 17 (𝐹:π΅βŸΆπ‘ƒ β†’ 𝐹 Fn 𝐡)
136132, 9, 1353syl 18 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝐹 Fn 𝐡)
137 simp-4r 782 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡))
138137simpld 493 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑠 ∈ 𝒫 𝐡)
139138elpwid 4615 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑠 βŠ† 𝐡)
140139adantlr 713 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑠 βŠ† 𝐡)
141 simprl 769 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘₯ ∈ 𝑠)
142 fnfvima 7251 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝐡 ∧ 𝑠 βŠ† 𝐡 ∧ π‘₯ ∈ 𝑠) β†’ (πΉβ€˜π‘₯) ∈ (𝐹 β€œ 𝑠))
143136, 140, 141, 142syl3anc 1368 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (πΉβ€˜π‘₯) ∈ (𝐹 β€œ 𝑠))
144137simprd 494 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 ∈ 𝒫 𝐡)
145144elpwid 4615 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 βŠ† 𝐡)
146145adantlr 713 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 βŠ† 𝐡)
147 simprr 771 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝑑)
148 fnfvima 7251 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝐡 ∧ 𝑑 βŠ† 𝐡 ∧ 𝑦 ∈ 𝑑) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ 𝑑))
149136, 146, 147, 148syl3anc 1368 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ 𝑑))
150 simplr 767 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓))
151 oveq1 7433 . . . . . . . . . . . . . . . . 17 (𝑒 = (πΉβ€˜π‘₯) β†’ (𝑒𝐼𝑓) = ((πΉβ€˜π‘₯)𝐼𝑓))
152151eleq2d 2815 . . . . . . . . . . . . . . . 16 (𝑒 = (πΉβ€˜π‘₯) β†’ (𝑐 ∈ (𝑒𝐼𝑓) ↔ 𝑐 ∈ ((πΉβ€˜π‘₯)𝐼𝑓)))
153 oveq2 7434 . . . . . . . . . . . . . . . . 17 (𝑓 = (πΉβ€˜π‘¦) β†’ ((πΉβ€˜π‘₯)𝐼𝑓) = ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦)))
154153eleq2d 2815 . . . . . . . . . . . . . . . 16 (𝑓 = (πΉβ€˜π‘¦) β†’ (𝑐 ∈ ((πΉβ€˜π‘₯)𝐼𝑓) ↔ 𝑐 ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦))))
155152, 154rspc2va 3623 . . . . . . . . . . . . . . 15 ((((πΉβ€˜π‘₯) ∈ (𝐹 β€œ 𝑠) ∧ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ 𝑑)) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ 𝑐 ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦)))
156143, 149, 150, 155syl21anc 836 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑐 ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦)))
157134, 156eqeltrd 2829 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦)))
1588ad4antr 730 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
159 simp-5l 783 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ πœ‘)
160159, 21sylancom 586 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
161 simp-5l 783 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ πœ‘)
162161, 23sylancom 586 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
163 simprl 769 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘₯ ∈ 𝑠)
164139, 163sseldd 3983 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘₯ ∈ 𝐡)
165 simprr 771 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝑑)
166145, 165sseldd 3983 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝐡)
16776ad4antr 730 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ ◑𝐹:π‘ƒβŸΆπ΅)
168 simplr 767 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑐 ∈ 𝑃)
169167, 168ffvelcdmd 7100 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (β—‘πΉβ€˜π‘) ∈ 𝐡)
1703, 4, 5, 17, 18, 19, 158, 160, 162, 164, 166, 169f1otrgitv 28694 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ ((β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦))))
171170adantlr 713 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ ((β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦))))
172157, 171mpbird 256 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦))
173172ralrimivva 3198 . . . . . . . . . . 11 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦))
174173adantllr 717 . . . . . . . . . 10 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦))
17576ad4antr 730 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) β†’ ◑𝐹:π‘ƒβŸΆπ΅)
176 simpr 483 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) β†’ 𝑐 ∈ 𝑃)
177175, 176ffvelcdmd 7100 . . . . . . . . . . . 12 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) β†’ (β—‘πΉβ€˜π‘) ∈ 𝐡)
178 eleq1 2817 . . . . . . . . . . . . . 14 (𝑏 = (β—‘πΉβ€˜π‘) β†’ (𝑏 ∈ (π‘₯𝐽𝑦) ↔ (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦)))
1791782ralbidv 3216 . . . . . . . . . . . . 13 (𝑏 = (β—‘πΉβ€˜π‘) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦) ↔ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦)))
180179adantl 480 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 = (β—‘πΉβ€˜π‘)) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦) ↔ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦)))
181177, 180rspcedv 3604 . . . . . . . . . . 11 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))
182181adantr 479 . . . . . . . . . 10 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))
183174, 182mpd 15 . . . . . . . . 9 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦))
1846ad3antrrr 728 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ 𝐺 ∈ TarskiG)
185 imassrn 6079 . . . . . . . . . . 11 (𝐹 β€œ 𝑠) βŠ† ran 𝐹
186 f1ofo 6851 . . . . . . . . . . . . 13 (𝐹:𝐡–1-1-onto→𝑃 β†’ 𝐹:𝐡–onto→𝑃)
187 forn 6819 . . . . . . . . . . . . 13 (𝐹:𝐡–onto→𝑃 β†’ ran 𝐹 = 𝑃)
1888, 186, 1873syl 18 . . . . . . . . . . . 12 (πœ‘ β†’ ran 𝐹 = 𝑃)
189188ad3antrrr 728 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ ran 𝐹 = 𝑃)
190185, 189sseqtrid 4034 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ (𝐹 β€œ 𝑠) βŠ† 𝑃)
191 imassrn 6079 . . . . . . . . . . 11 (𝐹 β€œ 𝑑) βŠ† ran 𝐹
192191, 189sseqtrid 4034 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ (𝐹 β€œ 𝑑) βŠ† 𝑃)
19310ad3antrrr 728 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
194 simplr 767 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ π‘Ž ∈ 𝐡)
195193, 194ffvelcdmd 7100 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ (πΉβ€˜π‘Ž) ∈ 𝑃)
1968ad5antr 732 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
197 ffn 6727 . . . . . . . . . . . . . . . . 17 (◑𝐹:π‘ƒβŸΆπ΅ β†’ ◑𝐹 Fn 𝑃)
198196, 74, 75, 1974syl 19 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ ◑𝐹 Fn 𝑃)
199190ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (𝐹 β€œ 𝑠) βŠ† 𝑃)
200 simplr 767 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑒 ∈ (𝐹 β€œ 𝑠))
201 fnfvima 7251 . . . . . . . . . . . . . . . 16 ((◑𝐹 Fn 𝑃 ∧ (𝐹 β€œ 𝑠) βŠ† 𝑃 ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) β†’ (β—‘πΉβ€˜π‘’) ∈ (◑𝐹 β€œ (𝐹 β€œ 𝑠)))
202198, 199, 200, 201syl3anc 1368 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘’) ∈ (◑𝐹 β€œ (𝐹 β€œ 𝑠)))
203196, 29syl 17 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝐹:𝐡–1-1→𝑃)
204 simp-5r 784 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡))
205204simpld 493 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑠 ∈ 𝒫 𝐡)
206205elpwid 4615 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑠 βŠ† 𝐡)
207 f1imacnv 6860 . . . . . . . . . . . . . . . 16 ((𝐹:𝐡–1-1→𝑃 ∧ 𝑠 βŠ† 𝐡) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑠)) = 𝑠)
208203, 206, 207syl2anc 582 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑠)) = 𝑠)
209202, 208eleqtrd 2831 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘’) ∈ 𝑠)
210192ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (𝐹 β€œ 𝑑) βŠ† 𝑃)
211 simpr 483 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑣 ∈ (𝐹 β€œ 𝑑))
212 fnfvima 7251 . . . . . . . . . . . . . . . 16 ((◑𝐹 Fn 𝑃 ∧ (𝐹 β€œ 𝑑) βŠ† 𝑃 ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘£) ∈ (◑𝐹 β€œ (𝐹 β€œ 𝑑)))
213198, 210, 211, 212syl3anc 1368 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘£) ∈ (◑𝐹 β€œ (𝐹 β€œ 𝑑)))
214204simprd 494 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑑 ∈ 𝒫 𝐡)
215214elpwid 4615 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑑 βŠ† 𝐡)
216 f1imacnv 6860 . . . . . . . . . . . . . . . 16 ((𝐹:𝐡–1-1→𝑃 ∧ 𝑑 βŠ† 𝐡) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑑)) = 𝑑)
217203, 215, 216syl2anc 582 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑑)) = 𝑑)
218213, 217eleqtrd 2831 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘£) ∈ 𝑑)
219 simpllr 774 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦))
220 eleq1 2817 . . . . . . . . . . . . . . 15 (π‘₯ = (β—‘πΉβ€˜π‘’) β†’ (π‘₯ ∈ (π‘Žπ½π‘¦) ↔ (β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½π‘¦)))
221 oveq2 7434 . . . . . . . . . . . . . . . 16 (𝑦 = (β—‘πΉβ€˜π‘£) β†’ (π‘Žπ½π‘¦) = (π‘Žπ½(β—‘πΉβ€˜π‘£)))
222221eleq2d 2815 . . . . . . . . . . . . . . 15 (𝑦 = (β—‘πΉβ€˜π‘£) β†’ ((β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½π‘¦) ↔ (β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½(β—‘πΉβ€˜π‘£))))
223220, 222rspc2va 3623 . . . . . . . . . . . . . 14 ((((β—‘πΉβ€˜π‘’) ∈ 𝑠 ∧ (β—‘πΉβ€˜π‘£) ∈ 𝑑) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ (β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½(β—‘πΉβ€˜π‘£)))
224209, 218, 219, 223syl21anc 836 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½(β—‘πΉβ€˜π‘£)))
225 simp-6l 785 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ πœ‘)
226225, 21sylancom 586 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
227 simp-6l 785 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ πœ‘)
228227, 23sylancom 586 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
229 simp-4r 782 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ π‘Ž ∈ 𝐡)
230210, 211sseldd 3983 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑣 ∈ 𝑃)
231 f1ocnvdm 7300 . . . . . . . . . . . . . . 15 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑣 ∈ 𝑃) β†’ (β—‘πΉβ€˜π‘£) ∈ 𝐡)
232196, 230, 231syl2anc 582 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘£) ∈ 𝐡)
233199, 200sseldd 3983 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑒 ∈ 𝑃)
234 f1ocnvdm 7300 . . . . . . . . . . . . . . 15 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑒 ∈ 𝑃) β†’ (β—‘πΉβ€˜π‘’) ∈ 𝐡)
235196, 233, 234syl2anc 582 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘’) ∈ 𝐡)
2363, 4, 5, 17, 18, 19, 196, 226, 228, 229, 232, 235f1otrgitv 28694 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ ((β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½(β—‘πΉβ€˜π‘£)) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘’)) ∈ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘£)))))
237224, 236mpbid 231 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘’)) ∈ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘£))))
238 f1ocnvfv2 7292 . . . . . . . . . . . . 13 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑒 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘’)) = 𝑒)
239196, 233, 238syl2anc 582 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘’)) = 𝑒)
240 f1ocnvfv2 7292 . . . . . . . . . . . . . 14 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑣 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘£)) = 𝑣)
241196, 230, 240syl2anc 582 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘£)) = 𝑣)
242241oveq2d 7442 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘£))) = ((πΉβ€˜π‘Ž)𝐼𝑣))
243237, 239, 2423eltr3d 2843 . . . . . . . . . . 11 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑒 ∈ ((πΉβ€˜π‘Ž)𝐼𝑣))
2442433impa 1107 . . . . . . . . . 10 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑒 ∈ ((πΉβ€˜π‘Ž)𝐼𝑣))
2453, 4, 5, 184, 190, 192, 195, 244axtgcont 28293 . . . . . . . . 9 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ βˆƒπ‘ ∈ 𝑃 βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓))
246183, 245r19.29a 3159 . . . . . . . 8 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦))
247246rexlimdva2 3154 . . . . . . 7 ((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) β†’ (βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))
248247ralrimivva 3198 . . . . . 6 (πœ‘ β†’ βˆ€π‘  ∈ 𝒫 π΅βˆ€π‘‘ ∈ 𝒫 𝐡(βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))
24973, 131, 2483jca 1125 . . . . 5 (πœ‘ β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽π‘₯) β†’ π‘₯ = 𝑦) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))) ∧ βˆ€π‘  ∈ 𝒫 π΅βˆ€π‘‘ ∈ 𝒫 𝐡(βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦))))
25017, 18, 19istrkgb 28279 . . . . 5 (𝐻 ∈ TarskiGB ↔ (𝐻 ∈ V ∧ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽π‘₯) β†’ π‘₯ = 𝑦) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))) ∧ βˆ€π‘  ∈ 𝒫 π΅βˆ€π‘‘ ∈ 𝒫 𝐡(βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))))
2512, 249, 250sylanbrc 581 . . . 4 (πœ‘ β†’ 𝐻 ∈ TarskiGB)
25256, 251elind 4196 . . 3 (πœ‘ β†’ 𝐻 ∈ (TarskiGC ∩ TarskiGB))
2536ad9antr 740 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝐺 ∈ TarskiG)
25410ad9antr 740 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝐹:π΅βŸΆπ‘ƒ)
255 simp-9r 792 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ π‘₯ ∈ 𝐡)
256254, 255ffvelcdmd 7100 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
257 simp-8r 790 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑦 ∈ 𝐡)
258254, 257ffvelcdmd 7100 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
259 simp-7r 788 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑧 ∈ 𝐡)
260254, 259ffvelcdmd 7100 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘§) ∈ 𝑃)
261 simp-5r 784 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ π‘Ž ∈ 𝐡)
262254, 261ffvelcdmd 7100 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘Ž) ∈ 𝑃)
263 simp-4r 782 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑏 ∈ 𝐡)
264254, 263ffvelcdmd 7100 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘) ∈ 𝑃)
265 simpllr 774 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑐 ∈ 𝐡)
266254, 265ffvelcdmd 7100 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘) ∈ 𝑃)
267 simp-6r 786 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑒 ∈ 𝐡)
268254, 267ffvelcdmd 7100 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘’) ∈ 𝑃)
269 simplr 767 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑣 ∈ 𝐡)
270254, 269ffvelcdmd 7100 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘£) ∈ 𝑃)
2718ad9antr 740 . . . . . . . . . . . . . . . . . . 19 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝐹:𝐡–1-1-onto→𝑃)
272271, 255jca 510 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡))
273 simprl1 1215 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ π‘₯ β‰  𝑦)
274 dff1o6 7290 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐡–1-1-onto→𝑃 ↔ (𝐹 Fn 𝐡 ∧ ran 𝐹 = 𝑃 ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦)))
275274simp3bi 1144 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝐡–1-1-onto→𝑃 β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦))
276275r19.21bi 3246 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦))
277276r19.21bi 3246 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) β†’ ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦))
278277necon3d 2958 . . . . . . . . . . . . . . . . . . 19 (((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) β†’ (π‘₯ β‰  𝑦 β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦)))
279278imp 405 . . . . . . . . . . . . . . . . . 18 ((((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ β‰  𝑦) β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦))
280272, 257, 273, 279syl21anc 836 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦))
281 simprl2 1216 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑦 ∈ (π‘₯𝐽𝑧))
28221ex 411 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“))))
283282ad9antr 740 . . . . . . . . . . . . . . . . . . . 20 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“))))
284283imp 405 . . . . . . . . . . . . . . . . . . 19 (((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
28523ex 411 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“)))))
286285ad9antr 740 . . . . . . . . . . . . . . . . . . . 20 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“)))))
287286imp 405 . . . . . . . . . . . . . . . . . . 19 (((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
2883, 4, 5, 17, 18, 19, 271, 284, 287, 255, 259, 257f1otrgitv 28694 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦 ∈ (π‘₯𝐽𝑧) ↔ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘§))))
289281, 288mpbid 231 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘§)))
290 simprl3 1217 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑏 ∈ (π‘Žπ½π‘))
2913, 4, 5, 17, 18, 19, 271, 284, 287, 261, 265, 263f1otrgitv 28694 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑏 ∈ (π‘Žπ½π‘) ↔ (πΉβ€˜π‘) ∈ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜π‘))))
292290, 291mpbid 231 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘) ∈ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜π‘)))
293 simprr 771 . . . . . . . . . . . . . . . . . . . 20 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))
294293simpld 493 . . . . . . . . . . . . . . . . . . 19 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)))
295294simpld 493 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘₯𝐸𝑦) = (π‘ŽπΈπ‘))
2963, 4, 5, 17, 18, 19, 271, 284, 287, 255, 257f1otrgds 28693 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘₯𝐸𝑦) = ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)))
2973, 4, 5, 17, 18, 19, 271, 284, 287, 261, 263f1otrgds 28693 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘ŽπΈπ‘) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
298295, 296, 2973eqtr3d 2776 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
299294simprd 494 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦𝐸𝑧) = (𝑏𝐸𝑐))
3003, 4, 5, 17, 18, 19, 271, 284, 287, 257, 259f1otrgds 28693 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦𝐸𝑧) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘§)))
3013, 4, 5, 17, 18, 19, 271, 284, 287, 263, 265f1otrgds 28693 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑏𝐸𝑐) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘)))
302299, 300, 3013eqtr3d 2776 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘§)) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘)))
303293simprd 494 . . . . . . . . . . . . . . . . . . 19 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))
304303simpld 493 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£))
3053, 4, 5, 17, 18, 19, 271, 284, 287, 255, 267f1otrgds 28693 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘₯𝐸𝑒) = ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘’)))
3063, 4, 5, 17, 18, 19, 271, 284, 287, 261, 269f1otrgds 28693 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘ŽπΈπ‘£) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘£)))
307304, 305, 3063eqtr3d 2776 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘’)) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘£)))
308303simprd 494 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))
3093, 4, 5, 17, 18, 19, 271, 284, 287, 257, 267f1otrgds 28693 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦𝐸𝑒) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘’)))
3103, 4, 5, 17, 18, 19, 271, 284, 287, 263, 269f1otrgds 28693 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑏𝐸𝑣) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘£)))
311308, 309, 3103eqtr3d 2776 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘’)) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘£)))
3123, 4, 5, 253, 256, 258, 260, 262, 264, 266, 268, 270, 280, 289, 292, 298, 302, 307, 311axtg5seg 28289 . . . . . . . . . . . . . . . 16 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘§)𝐷(πΉβ€˜π‘’)) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘£)))
3133, 4, 5, 17, 18, 19, 271, 284, 287, 259, 267f1otrgds 28693 . . . . . . . . . . . . . . . 16 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑧𝐸𝑒) = ((πΉβ€˜π‘§)𝐷(πΉβ€˜π‘’)))
3143, 4, 5, 17, 18, 19, 271, 284, 287, 265, 269f1otrgds 28693 . . . . . . . . . . . . . . . 16 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑐𝐸𝑣) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘£)))
315312, 313, 3143eqtr4d 2778 . . . . . . . . . . . . . . 15 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣))
316315ex 411 . . . . . . . . . . . . . 14 (((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) β†’ (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
317316ralrimiva 3143 . . . . . . . . . . . . 13 ((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) β†’ βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
318317ralrimiva 3143 . . . . . . . . . . . 12 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) β†’ βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
319318ralrimiva 3143 . . . . . . . . . . 11 ((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) β†’ βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
320319ralrimiva 3143 . . . . . . . . . 10 (((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
321320ralrimiva 3143 . . . . . . . . 9 ((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
322321ralrimiva 3143 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) β†’ βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
323322ralrimiva 3143 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
324323ralrimiva 3143 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
325 simp-4l 781 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ πœ‘)
326 simplr 767 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝑀 ∈ 𝑃)
327 simprl 769 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀))
328325, 8syl 17 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝐹:𝐡–1-1-onto→𝑃)
329 f1ocnvfv2 7292 . . . . . . . . . . . . . 14 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑀 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘€)) = 𝑀)
330328, 326, 329syl2anc 582 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘€)) = 𝑀)
331330oveq2d 7442 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘€))) = ((πΉβ€˜π‘₯)𝐼𝑀))
332327, 331eleqtrrd 2832 . . . . . . . . . . 11 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘€))))
333325, 21sylan 578 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
334325, 23sylan 578 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
33512ad3antrrr 728 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ π‘₯ ∈ 𝐡)
33676ffvelcdmda 7099 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ 𝑃) β†’ (β—‘πΉβ€˜π‘€) ∈ 𝐡)
337325, 326, 336syl2anc 582 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (β—‘πΉβ€˜π‘€) ∈ 𝐡)
33814ad3antrrr 728 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝑦 ∈ 𝐡)
3393, 4, 5, 17, 18, 19, 328, 333, 334, 335, 337, 338f1otrgitv 28694 . . . . . . . . . . 11 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ↔ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘€)))))
340332, 339mpbird 256 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)))
3413, 4, 5, 17, 18, 19, 328, 333, 334, 338, 337f1otrgds 28693 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜(β—‘πΉβ€˜π‘€))))
342330oveq2d 7442 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ ((πΉβ€˜π‘¦)𝐷(πΉβ€˜(β—‘πΉβ€˜π‘€))) = ((πΉβ€˜π‘¦)𝐷𝑀))
343 simprr 771 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
344341, 342, 3433eqtrd 2772 . . . . . . . . . . 11 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
345 simprl 769 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ π‘Ž ∈ 𝐡)
346345ad2antrr 724 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ π‘Ž ∈ 𝐡)
347 simprr 771 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ 𝑏 ∈ 𝐡)
348347ad2antrr 724 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝑏 ∈ 𝐡)
3493, 4, 5, 17, 18, 19, 328, 333, 334, 346, 348f1otrgds 28693 . . . . . . . . . . 11 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (π‘ŽπΈπ‘) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
350344, 349eqtr4d 2771 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘))
351 oveq2 7434 . . . . . . . . . . . . . . 15 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ (π‘₯𝐽𝑧) = (π‘₯𝐽(β—‘πΉβ€˜π‘€)))
352351eleq2d 2815 . . . . . . . . . . . . . 14 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ (𝑦 ∈ (π‘₯𝐽𝑧) ↔ 𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€))))
353 oveq2 7434 . . . . . . . . . . . . . . 15 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ (𝑦𝐸𝑧) = (𝑦𝐸(β—‘πΉβ€˜π‘€)))
354353eqeq1d 2730 . . . . . . . . . . . . . 14 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ ((𝑦𝐸𝑧) = (π‘ŽπΈπ‘) ↔ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘)))
355352, 354anbi12d 630 . . . . . . . . . . . . 13 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ ((𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)) ↔ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ∧ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘))))
356355adantl 480 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀 ∈ 𝑃) ∧ 𝑧 = (β—‘πΉβ€˜π‘€)) β†’ ((𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)) ↔ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ∧ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘))))
357336, 356rspcedv 3604 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ 𝑃) β†’ ((𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ∧ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘)) β†’ βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘))))
358357imp 405 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ 𝑃) ∧ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ∧ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘))) β†’ βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
359325, 326, 340, 350, 358syl22anc 837 . . . . . . . . 9 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
3607adantr 479 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ 𝐺 ∈ TarskiG)
36113adantr 479 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
36215adantr 479 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
36311adantr 479 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
364363, 345ffvelcdmd 7100 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ (πΉβ€˜π‘Ž) ∈ 𝑃)
365363, 347ffvelcdmd 7100 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ (πΉβ€˜π‘) ∈ 𝑃)
3663, 4, 5, 360, 361, 362, 364, 365axtgsegcon 28288 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ βˆƒπ‘€ ∈ 𝑃 ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘))))
367359, 366r19.29a 3159 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
368367ralrimivva 3198 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
369368ralrimivva 3198 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
3702, 324, 369jca32 514 . . . . 5 (πœ‘ β†’ (𝐻 ∈ V ∧ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))))
37117, 18, 19istrkgcb 28280 . . . . 5 (𝐻 ∈ TarskiGCB ↔ (𝐻 ∈ V ∧ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))))
372370, 371sylibr 233 . . . 4 (πœ‘ β†’ 𝐻 ∈ TarskiGCB)
373 f1otrg.l . . . . 5 (πœ‘ β†’ (LineGβ€˜π») = (π‘₯ ∈ 𝐡, 𝑦 ∈ (𝐡 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝐡 ∣ (𝑧 ∈ (π‘₯𝐽𝑦) ∨ π‘₯ ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (π‘₯𝐽𝑧))}))
37417, 18, 19istrkgl 28282 . . . . 5 (𝐻 ∈ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})} ↔ (𝐻 ∈ V ∧ (LineGβ€˜π») = (π‘₯ ∈ 𝐡, 𝑦 ∈ (𝐡 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝐡 ∣ (𝑧 ∈ (π‘₯𝐽𝑦) ∨ π‘₯ ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (π‘₯𝐽𝑧))})))
3752, 373, 374sylanbrc 581 . . . 4 (πœ‘ β†’ 𝐻 ∈ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})
376372, 375elind 4196 . . 3 (πœ‘ β†’ 𝐻 ∈ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
377252, 376elind 4196 . 2 (πœ‘ β†’ 𝐻 ∈ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})))
378 df-trkg 28277 . 2 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
379377, 378eleqtrrdi 2840 1 (πœ‘ β†’ 𝐻 ∈ TarskiG)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∨ w3o 1083   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  {cab 2705   β‰  wne 2937  βˆ€wral 3058  βˆƒwrex 3067  {crab 3430  Vcvv 3473  [wsbc 3778   βˆ– cdif 3946   ∩ cin 3948   βŠ† wss 3949  π’« cpw 4606  {csn 4632  β—‘ccnv 5681  ran crn 5683   β€œ cima 5685   Fn wfn 6548  βŸΆwf 6549  β€“1-1β†’wf1 6550  β€“ontoβ†’wfo 6551  β€“1-1-ontoβ†’wf1o 6552  β€˜cfv 6553  (class class class)co 7426   ∈ cmpo 7428  Basecbs 17187  distcds 17249  TarskiGcstrkg 28251  TarskiGCcstrkgc 28252  TarskiGBcstrkgb 28253  TarskiGCBcstrkgcb 28254  Itvcitv 28257  LineGclng 28258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-trkgc 28272  df-trkgb 28273  df-trkgcb 28274  df-trkg 28277
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator