MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1otrg Structured version   Visualization version   GIF version
Theorem f1otrg 28111
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 481 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ 𝐺 ∈ TarskiG)
8 f1otrkg.f . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹:𝐡–1-1-onto→𝑃)
9 f1of 6830 . . . . . . . . . . . 12 (𝐹:𝐡–1-1-onto→𝑃 β†’ 𝐹:π΅βŸΆπ‘ƒ)
108, 9syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹:π΅βŸΆπ‘ƒ)
1110adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
12 simprl 769 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ π‘₯ ∈ 𝐡)
1311, 12ffvelcdmd 7084 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
14 simprr 771 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ 𝑦 ∈ 𝐡)
1511, 14ffvelcdmd 7084 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
163, 4, 5, 7, 13, 15axtgcgrrflx 27702 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘₯)))
17 f1otrkg.b . . . . . . . . 9 𝐡 = (Baseβ€˜π»)
18 f1otrkg.e . . . . . . . . 9 𝐸 = (distβ€˜π»)
19 f1otrkg.j . . . . . . . . 9 𝐽 = (Itvβ€˜π»)
208adantr 481 . . . . . . . . 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 28109 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (π‘₯𝐸𝑦) = ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)))
263, 4, 5, 17, 18, 19, 20, 22, 24, 14, 12f1otrgds 28109 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (𝑦𝐸π‘₯) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘₯)))
2716, 25, 263eqtr4d 2782 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (π‘₯𝐸𝑦) = (𝑦𝐸π‘₯))
2827ralrimivva 3200 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (π‘₯𝐸𝑦) = (𝑦𝐸π‘₯))
29 f1of1 6829 . . . . . . . . . . 11 (𝐹:𝐡–1-1-onto→𝑃 β†’ 𝐹:𝐡–1-1→𝑃)
308, 29syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:𝐡–1-1→𝑃)
31303ad2ant1 1133 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝐹:𝐡–1-1→𝑃)
32 simp21 1206 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ π‘₯ ∈ 𝐡)
33 simp22 1207 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝑦 ∈ 𝐡)
3432, 33jca 512 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡))
3563ad2ant1 1133 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝐺 ∈ TarskiG)
36103ad2ant1 1133 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
3736, 32ffvelcdmd 7084 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
3836, 33ffvelcdmd 7084 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
39 simp23 1208 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝑧 ∈ 𝐡)
4036, 39ffvelcdmd 7084 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (πΉβ€˜π‘§) ∈ 𝑃)
41 simp3 1138 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧))
4283ad2ant1 1133 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
43213ad2antl1 1185 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
44233ad2antl1 1185 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
453, 4, 5, 17, 18, 19, 42, 43, 44, 32, 33f1otrgds 28109 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (π‘₯𝐸𝑦) = ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)))
463, 4, 5, 17, 18, 19, 42, 43, 44, 39, 39f1otrgds 28109 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (𝑧𝐸𝑧) = ((πΉβ€˜π‘§)𝐷(πΉβ€˜π‘§)))
4741, 45, 463eqtr3d 2780 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)) = ((πΉβ€˜π‘§)𝐷(πΉβ€˜π‘§)))
483, 4, 5, 35, 37, 38, 40, 47axtgcgrid 27703 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘¦))
49 f1veqaeq 7252 . . . . . . . . . 10 ((𝐹:𝐡–1-1→𝑃 ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦))
5049imp 407 . . . . . . . . 9 (((𝐹:𝐡–1-1→𝑃 ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (πΉβ€˜π‘₯) = (πΉβ€˜π‘¦)) β†’ π‘₯ = 𝑦)
5131, 34, 48, 50syl21anc 836 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ π‘₯ = 𝑦)
52513expia 1121 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((π‘₯𝐸𝑦) = (𝑧𝐸𝑧) β†’ π‘₯ = 𝑦))
5352ralrimivvva 3203 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 ((π‘₯𝐸𝑦) = (𝑧𝐸𝑧) β†’ π‘₯ = 𝑦))
5428, 53jca 512 . . . . 5 (πœ‘ β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (π‘₯𝐸𝑦) = (𝑦𝐸π‘₯) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 ((π‘₯𝐸𝑦) = (𝑧𝐸𝑧) β†’ π‘₯ = 𝑦)))
5517, 18, 19istrkgc 27694 . . . . 5 (𝐻 ∈ TarskiGC ↔ (𝐻 ∈ V ∧ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (π‘₯𝐸𝑦) = (𝑦𝐸π‘₯) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 ((π‘₯𝐸𝑦) = (𝑧𝐸𝑧) β†’ π‘₯ = 𝑦))))
562, 54, 55sylanbrc 583 . . . 4 (πœ‘ β†’ 𝐻 ∈ TarskiGC)
5783ad2ant1 1133 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
5857, 29syl 17 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ 𝐹:𝐡–1-1→𝑃)
59 simp2 1137 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡))
6063ad2ant1 1133 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ 𝐺 ∈ TarskiG)
61133adant3 1132 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
62153adant3 1132 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
63 simp3 1138 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ 𝑦 ∈ (π‘₯𝐽π‘₯))
64213ad2antl1 1185 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
65233ad2antl1 1185 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
66123adant3 1132 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ π‘₯ ∈ 𝐡)
67143adant3 1132 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ 𝑦 ∈ 𝐡)
683, 4, 5, 17, 18, 19, 57, 64, 65, 66, 66, 67f1otrgitv 28110 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (𝑦 ∈ (π‘₯𝐽π‘₯) ↔ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘₯))))
6963, 68mpbid 231 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘₯)))
703, 4, 5, 60, 61, 62, 69axtgbtwnid 27706 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘¦))
7158, 59, 70, 50syl21anc 836 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ π‘₯ = 𝑦)
72713expia 1121 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (𝑦 ∈ (π‘₯𝐽π‘₯) β†’ π‘₯ = 𝑦))
7372ralrimivva 3200 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽π‘₯) β†’ π‘₯ = 𝑦))
74 f1ocnv 6842 . . . . . . . . . . . . . 14 (𝐹:𝐡–1-1-onto→𝑃 β†’ ◑𝐹:𝑃–1-1-onto→𝐡)
75 f1of 6830 . . . . . . . . . . . . . 14 (◑𝐹:𝑃–1-1-onto→𝐡 β†’ ◑𝐹:π‘ƒβŸΆπ΅)
768, 74, 753syl 18 . . . . . . . . . . . . 13 (πœ‘ β†’ ◑𝐹:π‘ƒβŸΆπ΅)
7776ad5antr 732 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ◑𝐹:π‘ƒβŸΆπ΅)
78 simplr 767 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑐 ∈ 𝑃)
7977, 78ffvelcdmd 7084 . . . . . . . . . . 11 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (β—‘πΉβ€˜π‘) ∈ 𝐡)
80 simpr 485 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ π‘Ž = (β—‘πΉβ€˜π‘)) β†’ π‘Ž = (β—‘πΉβ€˜π‘))
8180eleq1d 2818 . . . . . . . . . . . 12 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ π‘Ž = (β—‘πΉβ€˜π‘)) β†’ (π‘Ž ∈ (𝑒𝐽𝑦) ↔ (β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦)))
8280eleq1d 2818 . . . . . . . . . . . 12 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ π‘Ž = (β—‘πΉβ€˜π‘)) β†’ (π‘Ž ∈ (𝑣𝐽π‘₯) ↔ (β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯)))
8381, 82anbi12d 631 . . . . . . . . . . 11 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ π‘Ž = (β—‘πΉβ€˜π‘)) β†’ ((π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯)) ↔ ((β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦) ∧ (β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯))))
84 simprl 769 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)))
8520ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝐹:𝐡–1-1-onto→𝑃)
8685ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝐹:𝐡–1-1-onto→𝑃)
87 f1ocnvfv2 7271 . . . . . . . . . . . . . . . 16 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) = 𝑐)
8887eleq1d 2818 . . . . . . . . . . . . . . 15 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) β†’ ((πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ↔ 𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦))))
8986, 78, 88syl2anc 584 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ↔ 𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦))))
9084, 89mpbird 256 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)))
9122ad4ant14 750 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
9291ad4ant14 750 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
9324ad4ant14 750 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
9493ad4ant14 750 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
95 simplr2 1216 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑒 ∈ 𝐡)
9695ad2antrr 724 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑒 ∈ 𝐡)
9714ad2antrr 724 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑦 ∈ 𝐡)
9897ad2antrr 724 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑦 ∈ 𝐡)
993, 4, 5, 17, 18, 19, 86, 92, 94, 96, 98, 79f1otrgitv 28110 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦))))
10090, 99mpbird 256 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦))
101 simprr 771 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))
10287eleq1d 2818 . . . . . . . . . . . . . . 15 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) β†’ ((πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)) ↔ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯))))
10386, 78, 102syl2anc 584 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)) ↔ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯))))
104101, 103mpbird 256 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))
105 simplr3 1217 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑣 ∈ 𝐡)
106105ad2antrr 724 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑣 ∈ 𝐡)
10712ad2antrr 724 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ π‘₯ ∈ 𝐡)
108107ad2antrr 724 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ π‘₯ ∈ 𝐡)
1093, 4, 5, 17, 18, 19, 86, 92, 94, 106, 108, 79f1otrgitv 28110 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯))))
110104, 109mpbird 256 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯))
111100, 110jca 512 . . . . . . . . . . 11 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦) ∧ (β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯)))
11279, 83, 111rspcedvd 3614 . . . . . . . . . 10 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯)))
1137ad2antrr 724 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝐺 ∈ TarskiG)
11411ad2antrr 724 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝐹:π΅βŸΆπ‘ƒ)
115114, 107ffvelcdmd 7084 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
116114, 97ffvelcdmd 7084 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
117 simplr1 1215 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑧 ∈ 𝐡)
118114, 117ffvelcdmd 7084 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘§) ∈ 𝑃)
119114, 95ffvelcdmd 7084 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘’) ∈ 𝑃)
120114, 105ffvelcdmd 7084 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘£) ∈ 𝑃)
121 simprl 769 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑒 ∈ (π‘₯𝐽𝑧))
1223, 4, 5, 17, 18, 19, 85, 91, 93, 107, 117, 95f1otrgitv 28110 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (𝑒 ∈ (π‘₯𝐽𝑧) ↔ (πΉβ€˜π‘’) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘§))))
123121, 122mpbid 231 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘’) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘§)))
124 simprr 771 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑣 ∈ (𝑦𝐽𝑧))
1253, 4, 5, 17, 18, 19, 85, 91, 93, 97, 117, 105f1otrgitv 28110 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (𝑣 ∈ (𝑦𝐽𝑧) ↔ (πΉβ€˜π‘£) ∈ ((πΉβ€˜π‘¦)𝐼(πΉβ€˜π‘§))))
126124, 125mpbid 231 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘£) ∈ ((πΉβ€˜π‘¦)𝐼(πΉβ€˜π‘§)))
1273, 4, 5, 113, 115, 116, 118, 119, 120, 123, 126axtgpasch 27707 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ βˆƒπ‘ ∈ 𝑃 (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯))))
128112, 127r19.29a 3162 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯)))
129128ex 413 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) β†’ ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))))
130129ralrimivvva 3203 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))))
131130ralrimivva 3200 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))))
1328ad5antr 732 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
133 simpllr 774 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑐 ∈ 𝑃)
134132, 133, 87syl2anc 584 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) = 𝑐)
135 ffn 6714 . . . . . . . . . . . . . . . . 17 (𝐹:π΅βŸΆπ‘ƒ β†’ 𝐹 Fn 𝐡)
136132, 9, 1353syl 18 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝐹 Fn 𝐡)
137 simp-4r 782 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡))
138137simpld 495 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑠 ∈ 𝒫 𝐡)
139138elpwid 4610 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑠 βŠ† 𝐡)
140139adantlr 713 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑠 βŠ† 𝐡)
141 simprl 769 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘₯ ∈ 𝑠)
142 fnfvima 7231 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝐡 ∧ 𝑠 βŠ† 𝐡 ∧ π‘₯ ∈ 𝑠) β†’ (πΉβ€˜π‘₯) ∈ (𝐹 β€œ 𝑠))
143136, 140, 141, 142syl3anc 1371 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (πΉβ€˜π‘₯) ∈ (𝐹 β€œ 𝑠))
144137simprd 496 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 ∈ 𝒫 𝐡)
145144elpwid 4610 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 βŠ† 𝐡)
146145adantlr 713 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 βŠ† 𝐡)
147 simprr 771 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝑑)
148 fnfvima 7231 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝐡 ∧ 𝑑 βŠ† 𝐡 ∧ 𝑦 ∈ 𝑑) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ 𝑑))
149136, 146, 147, 148syl3anc 1371 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ 𝑑))
150 simplr 767 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓))
151 oveq1 7412 . . . . . . . . . . . . . . . . 17 (𝑒 = (πΉβ€˜π‘₯) β†’ (𝑒𝐼𝑓) = ((πΉβ€˜π‘₯)𝐼𝑓))
152151eleq2d 2819 . . . . . . . . . . . . . . . 16 (𝑒 = (πΉβ€˜π‘₯) β†’ (𝑐 ∈ (𝑒𝐼𝑓) ↔ 𝑐 ∈ ((πΉβ€˜π‘₯)𝐼𝑓)))
153 oveq2 7413 . . . . . . . . . . . . . . . . 17 (𝑓 = (πΉβ€˜π‘¦) β†’ ((πΉβ€˜π‘₯)𝐼𝑓) = ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦)))
154153eleq2d 2819 . . . . . . . . . . . . . . . 16 (𝑓 = (πΉβ€˜π‘¦) β†’ (𝑐 ∈ ((πΉβ€˜π‘₯)𝐼𝑓) ↔ 𝑐 ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦))))
155152, 154rspc2va 3622 . . . . . . . . . . . . . . 15 ((((πΉβ€˜π‘₯) ∈ (𝐹 β€œ 𝑠) ∧ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ 𝑑)) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ 𝑐 ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦)))
156143, 149, 150, 155syl21anc 836 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑐 ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦)))
157134, 156eqeltrd 2833 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦)))
1588ad4antr 730 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
159 simp-5l 783 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ πœ‘)
160159, 21sylancom 588 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
161 simp-5l 783 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ πœ‘)
162161, 23sylancom 588 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
163 simprl 769 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘₯ ∈ 𝑠)
164139, 163sseldd 3982 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘₯ ∈ 𝐡)
165 simprr 771 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝑑)
166145, 165sseldd 3982 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝐡)
16776ad4antr 730 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ ◑𝐹:π‘ƒβŸΆπ΅)
168 simplr 767 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑐 ∈ 𝑃)
169167, 168ffvelcdmd 7084 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (β—‘πΉβ€˜π‘) ∈ 𝐡)
1703, 4, 5, 17, 18, 19, 158, 160, 162, 164, 166, 169f1otrgitv 28110 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ ((β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦))))
171170adantlr 713 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ ((β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦))))
172157, 171mpbird 256 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦))
173172ralrimivva 3200 . . . . . . . . . . 11 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦))
174173adantllr 717 . . . . . . . . . 10 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦))
17576ad4antr 730 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) β†’ ◑𝐹:π‘ƒβŸΆπ΅)
176 simpr 485 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) β†’ 𝑐 ∈ 𝑃)
177175, 176ffvelcdmd 7084 . . . . . . . . . . . 12 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) β†’ (β—‘πΉβ€˜π‘) ∈ 𝐡)
178 eleq1 2821 . . . . . . . . . . . . . 14 (𝑏 = (β—‘πΉβ€˜π‘) β†’ (𝑏 ∈ (π‘₯𝐽𝑦) ↔ (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦)))
1791782ralbidv 3218 . . . . . . . . . . . . 13 (𝑏 = (β—‘πΉβ€˜π‘) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦) ↔ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦)))
180179adantl 482 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 = (β—‘πΉβ€˜π‘)) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦) ↔ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦)))
181177, 180rspcedv 3605 . . . . . . . . . . 11 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))
182181adantr 481 . . . . . . . . . 10 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))
183174, 182mpd 15 . . . . . . . . 9 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦))
1846ad3antrrr 728 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ 𝐺 ∈ TarskiG)
185 imassrn 6068 . . . . . . . . . . 11 (𝐹 β€œ 𝑠) βŠ† ran 𝐹
186 f1ofo 6837 . . . . . . . . . . . . 13 (𝐹:𝐡–1-1-onto→𝑃 β†’ 𝐹:𝐡–onto→𝑃)
187 forn 6805 . . . . . . . . . . . . 13 (𝐹:𝐡–onto→𝑃 β†’ ran 𝐹 = 𝑃)
1888, 186, 1873syl 18 . . . . . . . . . . . 12 (πœ‘ β†’ ran 𝐹 = 𝑃)
189188ad3antrrr 728 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ ran 𝐹 = 𝑃)
190185, 189sseqtrid 4033 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ (𝐹 β€œ 𝑠) βŠ† 𝑃)
191 imassrn 6068 . . . . . . . . . . 11 (𝐹 β€œ 𝑑) βŠ† ran 𝐹
192191, 189sseqtrid 4033 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ (𝐹 β€œ 𝑑) βŠ† 𝑃)
19310ad3antrrr 728 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
194 simplr 767 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ π‘Ž ∈ 𝐡)
195193, 194ffvelcdmd 7084 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ (πΉβ€˜π‘Ž) ∈ 𝑃)
1968ad5antr 732 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
197 ffn 6714 . . . . . . . . . . . . . . . . 17 (◑𝐹:π‘ƒβŸΆπ΅ β†’ ◑𝐹 Fn 𝑃)
198196, 74, 75, 1974syl 19 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ ◑𝐹 Fn 𝑃)
199190ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (𝐹 β€œ 𝑠) βŠ† 𝑃)
200 simplr 767 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑒 ∈ (𝐹 β€œ 𝑠))
201 fnfvima 7231 . . . . . . . . . . . . . . . 16 ((◑𝐹 Fn 𝑃 ∧ (𝐹 β€œ 𝑠) βŠ† 𝑃 ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) β†’ (β—‘πΉβ€˜π‘’) ∈ (◑𝐹 β€œ (𝐹 β€œ 𝑠)))
202198, 199, 200, 201syl3anc 1371 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘’) ∈ (◑𝐹 β€œ (𝐹 β€œ 𝑠)))
203196, 29syl 17 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝐹:𝐡–1-1→𝑃)
204 simp-5r 784 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡))
205204simpld 495 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑠 ∈ 𝒫 𝐡)
206205elpwid 4610 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑠 βŠ† 𝐡)
207 f1imacnv 6846 . . . . . . . . . . . . . . . 16 ((𝐹:𝐡–1-1→𝑃 ∧ 𝑠 βŠ† 𝐡) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑠)) = 𝑠)
208203, 206, 207syl2anc 584 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑠)) = 𝑠)
209202, 208eleqtrd 2835 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘’) ∈ 𝑠)
210192ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (𝐹 β€œ 𝑑) βŠ† 𝑃)
211 simpr 485 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑣 ∈ (𝐹 β€œ 𝑑))
212 fnfvima 7231 . . . . . . . . . . . . . . . 16 ((◑𝐹 Fn 𝑃 ∧ (𝐹 β€œ 𝑑) βŠ† 𝑃 ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘£) ∈ (◑𝐹 β€œ (𝐹 β€œ 𝑑)))
213198, 210, 211, 212syl3anc 1371 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘£) ∈ (◑𝐹 β€œ (𝐹 β€œ 𝑑)))
214204simprd 496 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑑 ∈ 𝒫 𝐡)
215214elpwid 4610 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑑 βŠ† 𝐡)
216 f1imacnv 6846 . . . . . . . . . . . . . . . 16 ((𝐹:𝐡–1-1→𝑃 ∧ 𝑑 βŠ† 𝐡) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑑)) = 𝑑)
217203, 215, 216syl2anc 584 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑑)) = 𝑑)
218213, 217eleqtrd 2835 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘£) ∈ 𝑑)
219 simpllr 774 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦))
220 eleq1 2821 . . . . . . . . . . . . . . 15 (π‘₯ = (β—‘πΉβ€˜π‘’) β†’ (π‘₯ ∈ (π‘Žπ½π‘¦) ↔ (β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½π‘¦)))
221 oveq2 7413 . . . . . . . . . . . . . . . 16 (𝑦 = (β—‘πΉβ€˜π‘£) β†’ (π‘Žπ½π‘¦) = (π‘Žπ½(β—‘πΉβ€˜π‘£)))
222221eleq2d 2819 . . . . . . . . . . . . . . 15 (𝑦 = (β—‘πΉβ€˜π‘£) β†’ ((β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½π‘¦) ↔ (β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½(β—‘πΉβ€˜π‘£))))
223220, 222rspc2va 3622 . . . . . . . . . . . . . 14 ((((β—‘πΉβ€˜π‘’) ∈ 𝑠 ∧ (β—‘πΉβ€˜π‘£) ∈ 𝑑) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ (β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½(β—‘πΉβ€˜π‘£)))
224209, 218, 219, 223syl21anc 836 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½(β—‘πΉβ€˜π‘£)))
225 simp-6l 785 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ πœ‘)
226225, 21sylancom 588 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
227 simp-6l 785 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ πœ‘)
228227, 23sylancom 588 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
229 simp-4r 782 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ π‘Ž ∈ 𝐡)
230210, 211sseldd 3982 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑣 ∈ 𝑃)
231 f1ocnvdm 7279 . . . . . . . . . . . . . . 15 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑣 ∈ 𝑃) β†’ (β—‘πΉβ€˜π‘£) ∈ 𝐡)
232196, 230, 231syl2anc 584 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘£) ∈ 𝐡)
233199, 200sseldd 3982 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑒 ∈ 𝑃)
234 f1ocnvdm 7279 . . . . . . . . . . . . . . 15 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑒 ∈ 𝑃) β†’ (β—‘πΉβ€˜π‘’) ∈ 𝐡)
235196, 233, 234syl2anc 584 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘’) ∈ 𝐡)
2363, 4, 5, 17, 18, 19, 196, 226, 228, 229, 232, 235f1otrgitv 28110 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ ((β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½(β—‘πΉβ€˜π‘£)) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘’)) ∈ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘£)))))
237224, 236mpbid 231 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘’)) ∈ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘£))))
238 f1ocnvfv2 7271 . . . . . . . . . . . . 13 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑒 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘’)) = 𝑒)
239196, 233, 238syl2anc 584 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘’)) = 𝑒)
240 f1ocnvfv2 7271 . . . . . . . . . . . . . 14 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑣 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘£)) = 𝑣)
241196, 230, 240syl2anc 584 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘£)) = 𝑣)
242241oveq2d 7421 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘£))) = ((πΉβ€˜π‘Ž)𝐼𝑣))
243237, 239, 2423eltr3d 2847 . . . . . . . . . . 11 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑒 ∈ ((πΉβ€˜π‘Ž)𝐼𝑣))
2442433impa 1110 . . . . . . . . . 10 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑒 ∈ ((πΉβ€˜π‘Ž)𝐼𝑣))
2453, 4, 5, 184, 190, 192, 195, 244axtgcont 27709 . . . . . . . . 9 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ βˆƒπ‘ ∈ 𝑃 βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓))
246183, 245r19.29a 3162 . . . . . . . 8 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦))
247246rexlimdva2 3157 . . . . . . 7 ((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) β†’ (βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))
248247ralrimivva 3200 . . . . . 6 (πœ‘ β†’ βˆ€π‘  ∈ 𝒫 π΅βˆ€π‘‘ ∈ 𝒫 𝐡(βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))
24973, 131, 2483jca 1128 . . . . 5 (πœ‘ β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽π‘₯) β†’ π‘₯ = 𝑦) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))) ∧ βˆ€π‘  ∈ 𝒫 π΅βˆ€π‘‘ ∈ 𝒫 𝐡(βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦))))
25017, 18, 19istrkgb 27695 . . . . 5 (𝐻 ∈ TarskiGB ↔ (𝐻 ∈ V ∧ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽π‘₯) β†’ π‘₯ = 𝑦) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))) ∧ βˆ€π‘  ∈ 𝒫 π΅βˆ€π‘‘ ∈ 𝒫 𝐡(βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))))
2512, 249, 250sylanbrc 583 . . . 4 (πœ‘ β†’ 𝐻 ∈ TarskiGB)
25256, 251elind 4193 . . 3 (πœ‘ β†’ 𝐻 ∈ (TarskiGC ∩ TarskiGB))
2536ad9antr 740 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝐺 ∈ TarskiG)
25410ad9antr 740 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝐹:π΅βŸΆπ‘ƒ)
255 simp-9r 792 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ π‘₯ ∈ 𝐡)
256254, 255ffvelcdmd 7084 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
257 simp-8r 790 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑦 ∈ 𝐡)
258254, 257ffvelcdmd 7084 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
259 simp-7r 788 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑧 ∈ 𝐡)
260254, 259ffvelcdmd 7084 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘§) ∈ 𝑃)
261 simp-5r 784 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ π‘Ž ∈ 𝐡)
262254, 261ffvelcdmd 7084 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘Ž) ∈ 𝑃)
263 simp-4r 782 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑏 ∈ 𝐡)
264254, 263ffvelcdmd 7084 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘) ∈ 𝑃)
265 simpllr 774 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑐 ∈ 𝐡)
266254, 265ffvelcdmd 7084 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘) ∈ 𝑃)
267 simp-6r 786 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑒 ∈ 𝐡)
268254, 267ffvelcdmd 7084 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘’) ∈ 𝑃)
269 simplr 767 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑣 ∈ 𝐡)
270254, 269ffvelcdmd 7084 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘£) ∈ 𝑃)
2718ad9antr 740 . . . . . . . . . . . . . . . . . . 19 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝐹:𝐡–1-1-onto→𝑃)
272271, 255jca 512 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡))
273 simprl1 1218 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ π‘₯ β‰  𝑦)
274 dff1o6 7269 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐡–1-1-onto→𝑃 ↔ (𝐹 Fn 𝐡 ∧ ran 𝐹 = 𝑃 ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦)))
275274simp3bi 1147 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝐡–1-1-onto→𝑃 β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦))
276275r19.21bi 3248 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦))
277276r19.21bi 3248 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) β†’ ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦))
278277necon3d 2961 . . . . . . . . . . . . . . . . . . 19 (((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) β†’ (π‘₯ β‰  𝑦 β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦)))
279278imp 407 . . . . . . . . . . . . . . . . . 18 ((((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ β‰  𝑦) β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦))
280272, 257, 273, 279syl21anc 836 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦))
281 simprl2 1219 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑦 ∈ (π‘₯𝐽𝑧))
28221ex 413 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“))))
283282ad9antr 740 . . . . . . . . . . . . . . . . . . . 20 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“))))
284283imp 407 . . . . . . . . . . . . . . . . . . 19 (((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
28523ex 413 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“)))))
286285ad9antr 740 . . . . . . . . . . . . . . . . . . . 20 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“)))))
287286imp 407 . . . . . . . . . . . . . . . . . . 19 (((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
2883, 4, 5, 17, 18, 19, 271, 284, 287, 255, 259, 257f1otrgitv 28110 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦 ∈ (π‘₯𝐽𝑧) ↔ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘§))))
289281, 288mpbid 231 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘§)))
290 simprl3 1220 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑏 ∈ (π‘Žπ½π‘))
2913, 4, 5, 17, 18, 19, 271, 284, 287, 261, 265, 263f1otrgitv 28110 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑏 ∈ (π‘Žπ½π‘) ↔ (πΉβ€˜π‘) ∈ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜π‘))))
292290, 291mpbid 231 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘) ∈ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜π‘)))
293 simprr 771 . . . . . . . . . . . . . . . . . . . 20 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))
294293simpld 495 . . . . . . . . . . . . . . . . . . 19 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)))
295294simpld 495 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘₯𝐸𝑦) = (π‘ŽπΈπ‘))
2963, 4, 5, 17, 18, 19, 271, 284, 287, 255, 257f1otrgds 28109 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘₯𝐸𝑦) = ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)))
2973, 4, 5, 17, 18, 19, 271, 284, 287, 261, 263f1otrgds 28109 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘ŽπΈπ‘) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
298295, 296, 2973eqtr3d 2780 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
299294simprd 496 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦𝐸𝑧) = (𝑏𝐸𝑐))
3003, 4, 5, 17, 18, 19, 271, 284, 287, 257, 259f1otrgds 28109 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦𝐸𝑧) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘§)))
3013, 4, 5, 17, 18, 19, 271, 284, 287, 263, 265f1otrgds 28109 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑏𝐸𝑐) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘)))
302299, 300, 3013eqtr3d 2780 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘§)) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘)))
303293simprd 496 . . . . . . . . . . . . . . . . . . 19 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))
304303simpld 495 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£))
3053, 4, 5, 17, 18, 19, 271, 284, 287, 255, 267f1otrgds 28109 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘₯𝐸𝑒) = ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘’)))
3063, 4, 5, 17, 18, 19, 271, 284, 287, 261, 269f1otrgds 28109 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘ŽπΈπ‘£) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘£)))
307304, 305, 3063eqtr3d 2780 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘’)) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘£)))
308303simprd 496 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))
3093, 4, 5, 17, 18, 19, 271, 284, 287, 257, 267f1otrgds 28109 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦𝐸𝑒) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘’)))
3103, 4, 5, 17, 18, 19, 271, 284, 287, 263, 269f1otrgds 28109 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑏𝐸𝑣) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘£)))
311308, 309, 3103eqtr3d 2780 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘’)) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘£)))
3123, 4, 5, 253, 256, 258, 260, 262, 264, 266, 268, 270, 280, 289, 292, 298, 302, 307, 311axtg5seg 27705 . . . . . . . . . . . . . . . 16 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘§)𝐷(πΉβ€˜π‘’)) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘£)))
3133, 4, 5, 17, 18, 19, 271, 284, 287, 259, 267f1otrgds 28109 . . . . . . . . . . . . . . . 16 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑧𝐸𝑒) = ((πΉβ€˜π‘§)𝐷(πΉβ€˜π‘’)))
3143, 4, 5, 17, 18, 19, 271, 284, 287, 265, 269f1otrgds 28109 . . . . . . . . . . . . . . . 16 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑐𝐸𝑣) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘£)))
315312, 313, 3143eqtr4d 2782 . . . . . . . . . . . . . . 15 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣))
316315ex 413 . . . . . . . . . . . . . 14 (((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) β†’ (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
317316ralrimiva 3146 . . . . . . . . . . . . 13 ((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) β†’ βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
318317ralrimiva 3146 . . . . . . . . . . . 12 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) β†’ βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
319318ralrimiva 3146 . . . . . . . . . . 11 ((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) β†’ βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
320319ralrimiva 3146 . . . . . . . . . 10 (((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
321320ralrimiva 3146 . . . . . . . . 9 ((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
322321ralrimiva 3146 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) β†’ βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
323322ralrimiva 3146 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
324323ralrimiva 3146 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
325 simp-4l 781 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ πœ‘)
326 simplr 767 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝑀 ∈ 𝑃)
327 simprl 769 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀))
328325, 8syl 17 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝐹:𝐡–1-1-onto→𝑃)
329 f1ocnvfv2 7271 . . . . . . . . . . . . . 14 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑀 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘€)) = 𝑀)
330328, 326, 329syl2anc 584 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘€)) = 𝑀)
331330oveq2d 7421 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘€))) = ((πΉβ€˜π‘₯)𝐼𝑀))
332327, 331eleqtrrd 2836 . . . . . . . . . . 11 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘€))))
333325, 21sylan 580 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
334325, 23sylan 580 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
33512ad3antrrr 728 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ π‘₯ ∈ 𝐡)
33676ffvelcdmda 7083 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ 𝑃) β†’ (β—‘πΉβ€˜π‘€) ∈ 𝐡)
337325, 326, 336syl2anc 584 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (β—‘πΉβ€˜π‘€) ∈ 𝐡)
33814ad3antrrr 728 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝑦 ∈ 𝐡)
3393, 4, 5, 17, 18, 19, 328, 333, 334, 335, 337, 338f1otrgitv 28110 . . . . . . . . . . 11 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ↔ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘€)))))
340332, 339mpbird 256 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)))
3413, 4, 5, 17, 18, 19, 328, 333, 334, 338, 337f1otrgds 28109 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜(β—‘πΉβ€˜π‘€))))
342330oveq2d 7421 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ ((πΉβ€˜π‘¦)𝐷(πΉβ€˜(β—‘πΉβ€˜π‘€))) = ((πΉβ€˜π‘¦)𝐷𝑀))
343 simprr 771 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
344341, 342, 3433eqtrd 2776 . . . . . . . . . . 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 28109 . . . . . . . . . . 11 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (π‘ŽπΈπ‘) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
350344, 349eqtr4d 2775 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘))
351 oveq2 7413 . . . . . . . . . . . . . . 15 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ (π‘₯𝐽𝑧) = (π‘₯𝐽(β—‘πΉβ€˜π‘€)))
352351eleq2d 2819 . . . . . . . . . . . . . 14 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ (𝑦 ∈ (π‘₯𝐽𝑧) ↔ 𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€))))
353 oveq2 7413 . . . . . . . . . . . . . . 15 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ (𝑦𝐸𝑧) = (𝑦𝐸(β—‘πΉβ€˜π‘€)))
354353eqeq1d 2734 . . . . . . . . . . . . . 14 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ ((𝑦𝐸𝑧) = (π‘ŽπΈπ‘) ↔ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘)))
355352, 354anbi12d 631 . . . . . . . . . . . . 13 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ ((𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)) ↔ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ∧ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘))))
356355adantl 482 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀 ∈ 𝑃) ∧ 𝑧 = (β—‘πΉβ€˜π‘€)) β†’ ((𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)) ↔ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ∧ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘))))
357336, 356rspcedv 3605 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ 𝑃) β†’ ((𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ∧ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘)) β†’ βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘))))
358357imp 407 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ 𝑃) ∧ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ∧ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘))) β†’ βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
359325, 326, 340, 350, 358syl22anc 837 . . . . . . . . 9 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
3607adantr 481 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ 𝐺 ∈ TarskiG)
36113adantr 481 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
36215adantr 481 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
36311adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
364363, 345ffvelcdmd 7084 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ (πΉβ€˜π‘Ž) ∈ 𝑃)
365363, 347ffvelcdmd 7084 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ (πΉβ€˜π‘) ∈ 𝑃)
3663, 4, 5, 360, 361, 362, 364, 365axtgsegcon 27704 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ βˆƒπ‘€ ∈ 𝑃 ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘))))
367359, 366r19.29a 3162 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
368367ralrimivva 3200 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
369368ralrimivva 3200 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
3702, 324, 369jca32 516 . . . . 5 (πœ‘ β†’ (𝐻 ∈ V ∧ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))))
37117, 18, 19istrkgcb 27696 . . . . 5 (𝐻 ∈ TarskiGCB ↔ (𝐻 ∈ V ∧ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))))
372370, 371sylibr 233 . . . 4 (πœ‘ β†’ 𝐻 ∈ TarskiGCB)
373 f1otrg.l . . . . 5 (πœ‘ β†’ (LineGβ€˜π») = (π‘₯ ∈ 𝐡, 𝑦 ∈ (𝐡 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝐡 ∣ (𝑧 ∈ (π‘₯𝐽𝑦) ∨ π‘₯ ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (π‘₯𝐽𝑧))}))
37417, 18, 19istrkgl 27698 . . . . 5 (𝐻 ∈ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})} ↔ (𝐻 ∈ V ∧ (LineGβ€˜π») = (π‘₯ ∈ 𝐡, 𝑦 ∈ (𝐡 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝐡 ∣ (𝑧 ∈ (π‘₯𝐽𝑦) ∨ π‘₯ ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (π‘₯𝐽𝑧))})))
3752, 373, 374sylanbrc 583 . . . 4 (πœ‘ β†’ 𝐻 ∈ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})
376372, 375elind 4193 . . 3 (πœ‘ β†’ 𝐻 ∈ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
377252, 376elind 4193 . 2 (πœ‘ β†’ 𝐻 ∈ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})))
378 df-trkg 27693 . 2 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
379377, 378eleqtrrdi 2844 1 (πœ‘ β†’ 𝐻 ∈ TarskiG)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ w3o 1086   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  {cab 2709   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432  Vcvv 3474  [wsbc 3776   βˆ– cdif 3944   ∩ cin 3946   βŠ† wss 3947  π’« cpw 4601  {csn 4627  β—‘ccnv 5674  ran crn 5676   β€œ cima 5678   Fn wfn 6535  βŸΆwf 6536  β€“1-1β†’wf1 6537  β€“ontoβ†’wfo 6538  β€“1-1-ontoβ†’wf1o 6539  β€˜cfv 6540  (class class class)co 7405   ∈ cmpo 7407  Basecbs 17140  distcds 17202  TarskiGcstrkg 27667  TarskiGCcstrkgc 27668  TarskiGBcstrkgb 27669  TarskiGCBcstrkgcb 27670  Itvcitv 27673  LineGclng 27674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-trkgc 27688  df-trkgb 27689  df-trkgcb 27690  df-trkg 27693
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator