MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1otrg Structured version   Visualization version   GIF version
Theorem f1otrg 28626
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 3489 . . . . 5 (πœ‘ β†’ 𝐻 ∈ V)
3 f1otrkg.p . . . . . . . . 9 𝑃 = (Baseβ€˜πΊ)
4 f1otrkg.d . . . . . . . . 9 𝐷 = (distβ€˜πΊ)
5 f1otrkg.i . . . . . . . . 9 𝐼 = (Itvβ€˜πΊ)
6 f1otrg.g . . . . . . . . . 10 (πœ‘ β†’ 𝐺 ∈ TarskiG)
76adantr 480 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ 𝐺 ∈ TarskiG)
8 f1otrkg.f . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹:𝐡–1-1-onto→𝑃)
9 f1of 6826 . . . . . . . . . . . 12 (𝐹:𝐡–1-1-onto→𝑃 β†’ 𝐹:π΅βŸΆπ‘ƒ)
108, 9syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹:π΅βŸΆπ‘ƒ)
1110adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
12 simprl 768 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ π‘₯ ∈ 𝐡)
1311, 12ffvelcdmd 7080 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
14 simprr 770 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ 𝑦 ∈ 𝐡)
1511, 14ffvelcdmd 7080 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
163, 4, 5, 7, 13, 15axtgcgrrflx 28217 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘₯)))
17 f1otrkg.b . . . . . . . . 9 𝐡 = (Baseβ€˜π»)
18 f1otrkg.e . . . . . . . . 9 𝐸 = (distβ€˜π»)
19 f1otrkg.j . . . . . . . . 9 𝐽 = (Itvβ€˜π»)
208adantr 480 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
21 f1otrkg.1 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
2221adantlr 712 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
23 f1otrkg.2 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
2423adantlr 712 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
253, 4, 5, 17, 18, 19, 20, 22, 24, 12, 14f1otrgds 28624 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (π‘₯𝐸𝑦) = ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)))
263, 4, 5, 17, 18, 19, 20, 22, 24, 14, 12f1otrgds 28624 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (𝑦𝐸π‘₯) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘₯)))
2716, 25, 263eqtr4d 2776 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (π‘₯𝐸𝑦) = (𝑦𝐸π‘₯))
2827ralrimivva 3194 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (π‘₯𝐸𝑦) = (𝑦𝐸π‘₯))
29 f1of1 6825 . . . . . . . . . . 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 511 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡))
3563ad2ant1 1130 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝐺 ∈ TarskiG)
36103ad2ant1 1130 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
3736, 32ffvelcdmd 7080 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
3836, 33ffvelcdmd 7080 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
39 simp23 1205 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ 𝑧 ∈ 𝐡)
4036, 39ffvelcdmd 7080 . . . . . . . . . 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 28624 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (π‘₯𝐸𝑦) = ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)))
463, 4, 5, 17, 18, 19, 42, 43, 44, 39, 39f1otrgds 28624 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (𝑧𝐸𝑧) = ((πΉβ€˜π‘§)𝐷(πΉβ€˜π‘§)))
4741, 45, 463eqtr3d 2774 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)) = ((πΉβ€˜π‘§)𝐷(πΉβ€˜π‘§)))
483, 4, 5, 35, 37, 38, 40, 47axtgcgrid 28218 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘¦))
49 f1veqaeq 7251 . . . . . . . . . 10 ((𝐹:𝐡–1-1→𝑃 ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦))
5049imp 406 . . . . . . . . 9 (((𝐹:𝐡–1-1→𝑃 ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (πΉβ€˜π‘₯) = (πΉβ€˜π‘¦)) β†’ π‘₯ = 𝑦)
5131, 34, 48, 50syl21anc 835 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯𝐸𝑦) = (𝑧𝐸𝑧)) β†’ π‘₯ = 𝑦)
52513expia 1118 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((π‘₯𝐸𝑦) = (𝑧𝐸𝑧) β†’ π‘₯ = 𝑦))
5352ralrimivvva 3197 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 ((π‘₯𝐸𝑦) = (𝑧𝐸𝑧) β†’ π‘₯ = 𝑦))
5428, 53jca 511 . . . . 5 (πœ‘ β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (π‘₯𝐸𝑦) = (𝑦𝐸π‘₯) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 ((π‘₯𝐸𝑦) = (𝑧𝐸𝑧) β†’ π‘₯ = 𝑦)))
5517, 18, 19istrkgc 28209 . . . . 5 (𝐻 ∈ TarskiGC ↔ (𝐻 ∈ V ∧ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (π‘₯𝐸𝑦) = (𝑦𝐸π‘₯) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 ((π‘₯𝐸𝑦) = (𝑧𝐸𝑧) β†’ π‘₯ = 𝑦))))
562, 54, 55sylanbrc 582 . . . 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 28625 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (𝑦 ∈ (π‘₯𝐽π‘₯) ↔ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘₯))))
6963, 68mpbid 231 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘₯)))
703, 4, 5, 60, 61, 62, 69axtgbtwnid 28221 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘¦))
7158, 59, 70, 50syl21anc 835 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) ∧ 𝑦 ∈ (π‘₯𝐽π‘₯)) β†’ π‘₯ = 𝑦)
72713expia 1118 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (𝑦 ∈ (π‘₯𝐽π‘₯) β†’ π‘₯ = 𝑦))
7372ralrimivva 3194 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽π‘₯) β†’ π‘₯ = 𝑦))
74 f1ocnv 6838 . . . . . . . . . . . . . 14 (𝐹:𝐡–1-1-onto→𝑃 β†’ ◑𝐹:𝑃–1-1-onto→𝐡)
75 f1of 6826 . . . . . . . . . . . . . 14 (◑𝐹:𝑃–1-1-onto→𝐡 β†’ ◑𝐹:π‘ƒβŸΆπ΅)
768, 74, 753syl 18 . . . . . . . . . . . . 13 (πœ‘ β†’ ◑𝐹:π‘ƒβŸΆπ΅)
7776ad5antr 731 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ◑𝐹:π‘ƒβŸΆπ΅)
78 simplr 766 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑐 ∈ 𝑃)
7977, 78ffvelcdmd 7080 . . . . . . . . . . 11 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (β—‘πΉβ€˜π‘) ∈ 𝐡)
80 simpr 484 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ π‘Ž = (β—‘πΉβ€˜π‘)) β†’ π‘Ž = (β—‘πΉβ€˜π‘))
8180eleq1d 2812 . . . . . . . . . . . 12 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ π‘Ž = (β—‘πΉβ€˜π‘)) β†’ (π‘Ž ∈ (𝑒𝐽𝑦) ↔ (β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦)))
8280eleq1d 2812 . . . . . . . . . . . 12 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ π‘Ž = (β—‘πΉβ€˜π‘)) β†’ (π‘Ž ∈ (𝑣𝐽π‘₯) ↔ (β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯)))
8381, 82anbi12d 630 . . . . . . . . . . 11 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ π‘Ž = (β—‘πΉβ€˜π‘)) β†’ ((π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯)) ↔ ((β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦) ∧ (β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯))))
84 simprl 768 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)))
8520ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝐹:𝐡–1-1-onto→𝑃)
8685ad2antrr 723 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝐹:𝐡–1-1-onto→𝑃)
87 f1ocnvfv2 7270 . . . . . . . . . . . . . . . 16 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) = 𝑐)
8887eleq1d 2812 . . . . . . . . . . . . . . 15 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) β†’ ((πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ↔ 𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦))))
8986, 78, 88syl2anc 583 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ↔ 𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦))))
9084, 89mpbird 257 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)))
9122ad4ant14 749 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
9291ad4ant14 749 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
9324ad4ant14 749 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
9493ad4ant14 749 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
95 simplr2 1213 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑒 ∈ 𝐡)
9695ad2antrr 723 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑒 ∈ 𝐡)
9714ad2antrr 723 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑦 ∈ 𝐡)
9897ad2antrr 723 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑦 ∈ 𝐡)
993, 4, 5, 17, 18, 19, 86, 92, 94, 96, 98, 79f1otrgitv 28625 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦))))
10090, 99mpbird 257 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦))
101 simprr 770 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))
10287eleq1d 2812 . . . . . . . . . . . . . . 15 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) β†’ ((πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)) ↔ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯))))
10386, 78, 102syl2anc 583 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)) ↔ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯))))
104101, 103mpbird 257 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))
105 simplr3 1214 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑣 ∈ 𝐡)
106105ad2antrr 723 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ 𝑣 ∈ 𝐡)
10712ad2antrr 723 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ π‘₯ ∈ 𝐡)
108107ad2antrr 723 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ π‘₯ ∈ 𝐡)
1093, 4, 5, 17, 18, 19, 86, 92, 94, 106, 108, 79f1otrgitv 28625 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯))))
110104, 109mpbird 257 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ (β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯))
111100, 110jca 511 . . . . . . . . . . 11 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ ((β—‘πΉβ€˜π‘) ∈ (𝑒𝐽𝑦) ∧ (β—‘πΉβ€˜π‘) ∈ (𝑣𝐽π‘₯)))
11279, 83, 111rspcedvd 3608 . . . . . . . . . 10 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯)))) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯)))
1137ad2antrr 723 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝐺 ∈ TarskiG)
11411ad2antrr 723 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝐹:π΅βŸΆπ‘ƒ)
115114, 107ffvelcdmd 7080 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
116114, 97ffvelcdmd 7080 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
117 simplr1 1212 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑧 ∈ 𝐡)
118114, 117ffvelcdmd 7080 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘§) ∈ 𝑃)
119114, 95ffvelcdmd 7080 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘’) ∈ 𝑃)
120114, 105ffvelcdmd 7080 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘£) ∈ 𝑃)
121 simprl 768 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑒 ∈ (π‘₯𝐽𝑧))
1223, 4, 5, 17, 18, 19, 85, 91, 93, 107, 117, 95f1otrgitv 28625 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (𝑒 ∈ (π‘₯𝐽𝑧) ↔ (πΉβ€˜π‘’) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘§))))
123121, 122mpbid 231 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘’) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘§)))
124 simprr 770 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ 𝑣 ∈ (𝑦𝐽𝑧))
1253, 4, 5, 17, 18, 19, 85, 91, 93, 97, 117, 105f1otrgitv 28625 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (𝑣 ∈ (𝑦𝐽𝑧) ↔ (πΉβ€˜π‘£) ∈ ((πΉβ€˜π‘¦)𝐼(πΉβ€˜π‘§))))
126124, 125mpbid 231 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ (πΉβ€˜π‘£) ∈ ((πΉβ€˜π‘¦)𝐼(πΉβ€˜π‘§)))
1273, 4, 5, 113, 115, 116, 118, 119, 120, 123, 126axtgpasch 28222 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ βˆƒπ‘ ∈ 𝑃 (𝑐 ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘¦)) ∧ 𝑐 ∈ ((πΉβ€˜π‘£)𝐼(πΉβ€˜π‘₯))))
128112, 127r19.29a 3156 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯)))
129128ex 412 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) β†’ ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))))
130129ralrimivvva 3197 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))))
131130ralrimivva 3194 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))))
1328ad5antr 731 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
133 simpllr 773 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑐 ∈ 𝑃)
134132, 133, 87syl2anc 583 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) = 𝑐)
135 ffn 6710 . . . . . . . . . . . . . . . . 17 (𝐹:π΅βŸΆπ‘ƒ β†’ 𝐹 Fn 𝐡)
136132, 9, 1353syl 18 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝐹 Fn 𝐡)
137 simp-4r 781 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡))
138137simpld 494 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑠 ∈ 𝒫 𝐡)
139138elpwid 4606 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑠 βŠ† 𝐡)
140139adantlr 712 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑠 βŠ† 𝐡)
141 simprl 768 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘₯ ∈ 𝑠)
142 fnfvima 7229 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝐡 ∧ 𝑠 βŠ† 𝐡 ∧ π‘₯ ∈ 𝑠) β†’ (πΉβ€˜π‘₯) ∈ (𝐹 β€œ 𝑠))
143136, 140, 141, 142syl3anc 1368 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (πΉβ€˜π‘₯) ∈ (𝐹 β€œ 𝑠))
144137simprd 495 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 ∈ 𝒫 𝐡)
145144elpwid 4606 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 βŠ† 𝐡)
146145adantlr 712 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 βŠ† 𝐡)
147 simprr 770 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝑑)
148 fnfvima 7229 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝐡 ∧ 𝑑 βŠ† 𝐡 ∧ 𝑦 ∈ 𝑑) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ 𝑑))
149136, 146, 147, 148syl3anc 1368 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ 𝑑))
150 simplr 766 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓))
151 oveq1 7411 . . . . . . . . . . . . . . . . 17 (𝑒 = (πΉβ€˜π‘₯) β†’ (𝑒𝐼𝑓) = ((πΉβ€˜π‘₯)𝐼𝑓))
152151eleq2d 2813 . . . . . . . . . . . . . . . 16 (𝑒 = (πΉβ€˜π‘₯) β†’ (𝑐 ∈ (𝑒𝐼𝑓) ↔ 𝑐 ∈ ((πΉβ€˜π‘₯)𝐼𝑓)))
153 oveq2 7412 . . . . . . . . . . . . . . . . 17 (𝑓 = (πΉβ€˜π‘¦) β†’ ((πΉβ€˜π‘₯)𝐼𝑓) = ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦)))
154153eleq2d 2813 . . . . . . . . . . . . . . . 16 (𝑓 = (πΉβ€˜π‘¦) β†’ (𝑐 ∈ ((πΉβ€˜π‘₯)𝐼𝑓) ↔ 𝑐 ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦))))
155152, 154rspc2va 3618 . . . . . . . . . . . . . . 15 ((((πΉβ€˜π‘₯) ∈ (𝐹 β€œ 𝑠) ∧ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ 𝑑)) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ 𝑐 ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦)))
156143, 149, 150, 155syl21anc 835 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑐 ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦)))
157134, 156eqeltrd 2827 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦)))
1588ad4antr 729 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
159 simp-5l 782 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ πœ‘)
160159, 21sylancom 587 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
161 simp-5l 782 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ πœ‘)
162161, 23sylancom 587 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
163 simprl 768 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘₯ ∈ 𝑠)
164139, 163sseldd 3978 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ π‘₯ ∈ 𝐡)
165 simprr 770 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝑑)
166145, 165sseldd 3978 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝐡)
16776ad4antr 729 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ ◑𝐹:π‘ƒβŸΆπ΅)
168 simplr 766 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑐 ∈ 𝑃)
169167, 168ffvelcdmd 7080 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (β—‘πΉβ€˜π‘) ∈ 𝐡)
1703, 4, 5, 17, 18, 19, 158, 160, 162, 164, 166, 169f1otrgitv 28625 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ ((β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦))))
171170adantlr 712 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ ((β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘)) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘¦))))
172157, 171mpbird 257 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (π‘₯ ∈ 𝑠 ∧ 𝑦 ∈ 𝑑)) β†’ (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦))
173172ralrimivva 3194 . . . . . . . . . . 11 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦))
174173adantllr 716 . . . . . . . . . 10 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦))
17576ad4antr 729 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) β†’ ◑𝐹:π‘ƒβŸΆπ΅)
176 simpr 484 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) β†’ 𝑐 ∈ 𝑃)
177175, 176ffvelcdmd 7080 . . . . . . . . . . . 12 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) β†’ (β—‘πΉβ€˜π‘) ∈ 𝐡)
178 eleq1 2815 . . . . . . . . . . . . . 14 (𝑏 = (β—‘πΉβ€˜π‘) β†’ (𝑏 ∈ (π‘₯𝐽𝑦) ↔ (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦)))
1791782ralbidv 3212 . . . . . . . . . . . . 13 (𝑏 = (β—‘πΉβ€˜π‘) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦) ↔ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦)))
180179adantl 481 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 = (β—‘πΉβ€˜π‘)) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦) ↔ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦)))
181177, 180rspcedv 3599 . . . . . . . . . . 11 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))
182181adantr 480 . . . . . . . . . 10 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ (βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 (β—‘πΉβ€˜π‘) ∈ (π‘₯𝐽𝑦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))
183174, 182mpd 15 . . . . . . . . 9 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑐 ∈ 𝑃) ∧ βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓)) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦))
1846ad3antrrr 727 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ 𝐺 ∈ TarskiG)
185 imassrn 6063 . . . . . . . . . . 11 (𝐹 β€œ 𝑠) βŠ† ran 𝐹
186 f1ofo 6833 . . . . . . . . . . . . 13 (𝐹:𝐡–1-1-onto→𝑃 β†’ 𝐹:𝐡–onto→𝑃)
187 forn 6801 . . . . . . . . . . . . 13 (𝐹:𝐡–onto→𝑃 β†’ ran 𝐹 = 𝑃)
1888, 186, 1873syl 18 . . . . . . . . . . . 12 (πœ‘ β†’ ran 𝐹 = 𝑃)
189188ad3antrrr 727 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ ran 𝐹 = 𝑃)
190185, 189sseqtrid 4029 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ (𝐹 β€œ 𝑠) βŠ† 𝑃)
191 imassrn 6063 . . . . . . . . . . 11 (𝐹 β€œ 𝑑) βŠ† ran 𝐹
192191, 189sseqtrid 4029 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ (𝐹 β€œ 𝑑) βŠ† 𝑃)
19310ad3antrrr 727 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
194 simplr 766 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ π‘Ž ∈ 𝐡)
195193, 194ffvelcdmd 7080 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ (πΉβ€˜π‘Ž) ∈ 𝑃)
1968ad5antr 731 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
197 ffn 6710 . . . . . . . . . . . . . . . . 17 (◑𝐹:π‘ƒβŸΆπ΅ β†’ ◑𝐹 Fn 𝑃)
198196, 74, 75, 1974syl 19 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ ◑𝐹 Fn 𝑃)
199190ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (𝐹 β€œ 𝑠) βŠ† 𝑃)
200 simplr 766 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑒 ∈ (𝐹 β€œ 𝑠))
201 fnfvima 7229 . . . . . . . . . . . . . . . 16 ((◑𝐹 Fn 𝑃 ∧ (𝐹 β€œ 𝑠) βŠ† 𝑃 ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) β†’ (β—‘πΉβ€˜π‘’) ∈ (◑𝐹 β€œ (𝐹 β€œ 𝑠)))
202198, 199, 200, 201syl3anc 1368 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘’) ∈ (◑𝐹 β€œ (𝐹 β€œ 𝑠)))
203196, 29syl 17 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝐹:𝐡–1-1→𝑃)
204 simp-5r 783 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡))
205204simpld 494 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑠 ∈ 𝒫 𝐡)
206205elpwid 4606 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑠 βŠ† 𝐡)
207 f1imacnv 6842 . . . . . . . . . . . . . . . 16 ((𝐹:𝐡–1-1→𝑃 ∧ 𝑠 βŠ† 𝐡) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑠)) = 𝑠)
208203, 206, 207syl2anc 583 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑠)) = 𝑠)
209202, 208eleqtrd 2829 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘’) ∈ 𝑠)
210192ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (𝐹 β€œ 𝑑) βŠ† 𝑃)
211 simpr 484 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑣 ∈ (𝐹 β€œ 𝑑))
212 fnfvima 7229 . . . . . . . . . . . . . . . 16 ((◑𝐹 Fn 𝑃 ∧ (𝐹 β€œ 𝑑) βŠ† 𝑃 ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘£) ∈ (◑𝐹 β€œ (𝐹 β€œ 𝑑)))
213198, 210, 211, 212syl3anc 1368 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘£) ∈ (◑𝐹 β€œ (𝐹 β€œ 𝑑)))
214204simprd 495 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑑 ∈ 𝒫 𝐡)
215214elpwid 4606 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑑 βŠ† 𝐡)
216 f1imacnv 6842 . . . . . . . . . . . . . . . 16 ((𝐹:𝐡–1-1→𝑃 ∧ 𝑑 βŠ† 𝐡) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑑)) = 𝑑)
217203, 215, 216syl2anc 583 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑑)) = 𝑑)
218213, 217eleqtrd 2829 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘£) ∈ 𝑑)
219 simpllr 773 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦))
220 eleq1 2815 . . . . . . . . . . . . . . 15 (π‘₯ = (β—‘πΉβ€˜π‘’) β†’ (π‘₯ ∈ (π‘Žπ½π‘¦) ↔ (β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½π‘¦)))
221 oveq2 7412 . . . . . . . . . . . . . . . 16 (𝑦 = (β—‘πΉβ€˜π‘£) β†’ (π‘Žπ½π‘¦) = (π‘Žπ½(β—‘πΉβ€˜π‘£)))
222221eleq2d 2813 . . . . . . . . . . . . . . 15 (𝑦 = (β—‘πΉβ€˜π‘£) β†’ ((β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½π‘¦) ↔ (β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½(β—‘πΉβ€˜π‘£))))
223220, 222rspc2va 3618 . . . . . . . . . . . . . 14 ((((β—‘πΉβ€˜π‘’) ∈ 𝑠 ∧ (β—‘πΉβ€˜π‘£) ∈ 𝑑) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ (β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½(β—‘πΉβ€˜π‘£)))
224209, 218, 219, 223syl21anc 835 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½(β—‘πΉβ€˜π‘£)))
225 simp-6l 784 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ πœ‘)
226225, 21sylancom 587 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
227 simp-6l 784 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ πœ‘)
228227, 23sylancom 587 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
229 simp-4r 781 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ π‘Ž ∈ 𝐡)
230210, 211sseldd 3978 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑣 ∈ 𝑃)
231 f1ocnvdm 7278 . . . . . . . . . . . . . . 15 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑣 ∈ 𝑃) β†’ (β—‘πΉβ€˜π‘£) ∈ 𝐡)
232196, 230, 231syl2anc 583 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘£) ∈ 𝐡)
233199, 200sseldd 3978 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑒 ∈ 𝑃)
234 f1ocnvdm 7278 . . . . . . . . . . . . . . 15 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑒 ∈ 𝑃) β†’ (β—‘πΉβ€˜π‘’) ∈ 𝐡)
235196, 233, 234syl2anc 583 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (β—‘πΉβ€˜π‘’) ∈ 𝐡)
2363, 4, 5, 17, 18, 19, 196, 226, 228, 229, 232, 235f1otrgitv 28625 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ ((β—‘πΉβ€˜π‘’) ∈ (π‘Žπ½(β—‘πΉβ€˜π‘£)) ↔ (πΉβ€˜(β—‘πΉβ€˜π‘’)) ∈ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘£)))))
237224, 236mpbid 231 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘’)) ∈ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘£))))
238 f1ocnvfv2 7270 . . . . . . . . . . . . 13 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑒 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘’)) = 𝑒)
239196, 233, 238syl2anc 583 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘’)) = 𝑒)
240 f1ocnvfv2 7270 . . . . . . . . . . . . . 14 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑣 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘£)) = 𝑣)
241196, 230, 240syl2anc 583 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘£)) = 𝑣)
242241oveq2d 7420 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘£))) = ((πΉβ€˜π‘Ž)𝐼𝑣))
243237, 239, 2423eltr3d 2841 . . . . . . . . . . 11 ((((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠)) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑒 ∈ ((πΉβ€˜π‘Ž)𝐼𝑣))
2442433impa 1107 . . . . . . . . . 10 (((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) ∧ 𝑒 ∈ (𝐹 β€œ 𝑠) ∧ 𝑣 ∈ (𝐹 β€œ 𝑑)) β†’ 𝑒 ∈ ((πΉβ€˜π‘Ž)𝐼𝑣))
2453, 4, 5, 184, 190, 192, 195, 244axtgcont 28224 . . . . . . . . 9 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ βˆƒπ‘ ∈ 𝑃 βˆ€π‘’ ∈ (𝐹 β€œ 𝑠)βˆ€π‘“ ∈ (𝐹 β€œ 𝑑)𝑐 ∈ (𝑒𝐼𝑓))
246183, 245r19.29a 3156 . . . . . . . 8 ((((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) ∧ π‘Ž ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦)) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦))
247246rexlimdva2 3151 . . . . . . 7 ((πœ‘ ∧ (𝑠 ∈ 𝒫 𝐡 ∧ 𝑑 ∈ 𝒫 𝐡)) β†’ (βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))
248247ralrimivva 3194 . . . . . 6 (πœ‘ β†’ βˆ€π‘  ∈ 𝒫 π΅βˆ€π‘‘ ∈ 𝒫 𝐡(βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))
24973, 131, 2483jca 1125 . . . . 5 (πœ‘ β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽π‘₯) β†’ π‘₯ = 𝑦) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))) ∧ βˆ€π‘  ∈ 𝒫 π΅βˆ€π‘‘ ∈ 𝒫 𝐡(βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦))))
25017, 18, 19istrkgb 28210 . . . . 5 (𝐻 ∈ TarskiGB ↔ (𝐻 ∈ V ∧ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽π‘₯) β†’ π‘₯ = 𝑦) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) β†’ βˆƒπ‘Ž ∈ 𝐡 (π‘Ž ∈ (𝑒𝐽𝑦) ∧ π‘Ž ∈ (𝑣𝐽π‘₯))) ∧ βˆ€π‘  ∈ 𝒫 π΅βˆ€π‘‘ ∈ 𝒫 𝐡(βˆƒπ‘Ž ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ½π‘¦) β†’ βˆƒπ‘ ∈ 𝐡 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝐽𝑦)))))
2512, 249, 250sylanbrc 582 . . . 4 (πœ‘ β†’ 𝐻 ∈ TarskiGB)
25256, 251elind 4189 . . 3 (πœ‘ β†’ 𝐻 ∈ (TarskiGC ∩ TarskiGB))
2536ad9antr 739 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝐺 ∈ TarskiG)
25410ad9antr 739 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝐹:π΅βŸΆπ‘ƒ)
255 simp-9r 791 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ π‘₯ ∈ 𝐡)
256254, 255ffvelcdmd 7080 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
257 simp-8r 789 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑦 ∈ 𝐡)
258254, 257ffvelcdmd 7080 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
259 simp-7r 787 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑧 ∈ 𝐡)
260254, 259ffvelcdmd 7080 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘§) ∈ 𝑃)
261 simp-5r 783 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ π‘Ž ∈ 𝐡)
262254, 261ffvelcdmd 7080 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘Ž) ∈ 𝑃)
263 simp-4r 781 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑏 ∈ 𝐡)
264254, 263ffvelcdmd 7080 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘) ∈ 𝑃)
265 simpllr 773 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑐 ∈ 𝐡)
266254, 265ffvelcdmd 7080 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘) ∈ 𝑃)
267 simp-6r 785 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑒 ∈ 𝐡)
268254, 267ffvelcdmd 7080 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘’) ∈ 𝑃)
269 simplr 766 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑣 ∈ 𝐡)
270254, 269ffvelcdmd 7080 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘£) ∈ 𝑃)
2718ad9antr 739 . . . . . . . . . . . . . . . . . . 19 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝐹:𝐡–1-1-onto→𝑃)
272271, 255jca 511 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡))
273 simprl1 1215 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ π‘₯ β‰  𝑦)
274 dff1o6 7268 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐡–1-1-onto→𝑃 ↔ (𝐹 Fn 𝐡 ∧ ran 𝐹 = 𝑃 ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦)))
275274simp3bi 1144 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝐡–1-1-onto→𝑃 β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦))
276275r19.21bi 3242 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦))
277276r19.21bi 3242 . . . . . . . . . . . . . . . . . . . 20 (((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) β†’ ((πΉβ€˜π‘₯) = (πΉβ€˜π‘¦) β†’ π‘₯ = 𝑦))
278277necon3d 2955 . . . . . . . . . . . . . . . . . . 19 (((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) β†’ (π‘₯ β‰  𝑦 β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦)))
279278imp 406 . . . . . . . . . . . . . . . . . 18 ((((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ π‘₯ β‰  𝑦) β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦))
280272, 257, 273, 279syl21anc 835 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦))
281 simprl2 1216 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑦 ∈ (π‘₯𝐽𝑧))
28221ex 412 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“))))
283282ad9antr 739 . . . . . . . . . . . . . . . . . . . 20 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“))))
284283imp 406 . . . . . . . . . . . . . . . . . . 19 (((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
28523ex 412 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“)))))
286285ad9antr 739 . . . . . . . . . . . . . . . . . . . 20 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“)))))
287286imp 406 . . . . . . . . . . . . . . . . . . 19 (((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
2883, 4, 5, 17, 18, 19, 271, 284, 287, 255, 259, 257f1otrgitv 28625 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦 ∈ (π‘₯𝐽𝑧) ↔ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘§))))
289281, 288mpbid 231 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘§)))
290 simprl3 1217 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ 𝑏 ∈ (π‘Žπ½π‘))
2913, 4, 5, 17, 18, 19, 271, 284, 287, 261, 265, 263f1otrgitv 28625 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑏 ∈ (π‘Žπ½π‘) ↔ (πΉβ€˜π‘) ∈ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜π‘))))
292290, 291mpbid 231 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (πΉβ€˜π‘) ∈ ((πΉβ€˜π‘Ž)𝐼(πΉβ€˜π‘)))
293 simprr 770 . . . . . . . . . . . . . . . . . . . 20 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))
294293simpld 494 . . . . . . . . . . . . . . . . . . 19 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)))
295294simpld 494 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘₯𝐸𝑦) = (π‘ŽπΈπ‘))
2963, 4, 5, 17, 18, 19, 271, 284, 287, 255, 257f1otrgds 28624 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘₯𝐸𝑦) = ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)))
2973, 4, 5, 17, 18, 19, 271, 284, 287, 261, 263f1otrgds 28624 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘ŽπΈπ‘) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
298295, 296, 2973eqtr3d 2774 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘¦)) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
299294simprd 495 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦𝐸𝑧) = (𝑏𝐸𝑐))
3003, 4, 5, 17, 18, 19, 271, 284, 287, 257, 259f1otrgds 28624 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦𝐸𝑧) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘§)))
3013, 4, 5, 17, 18, 19, 271, 284, 287, 263, 265f1otrgds 28624 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑏𝐸𝑐) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘)))
302299, 300, 3013eqtr3d 2774 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘§)) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘)))
303293simprd 495 . . . . . . . . . . . . . . . . . . 19 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))
304303simpld 494 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£))
3053, 4, 5, 17, 18, 19, 271, 284, 287, 255, 267f1otrgds 28624 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘₯𝐸𝑒) = ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘’)))
3063, 4, 5, 17, 18, 19, 271, 284, 287, 261, 269f1otrgds 28624 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (π‘ŽπΈπ‘£) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘£)))
307304, 305, 3063eqtr3d 2774 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘₯)𝐷(πΉβ€˜π‘’)) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘£)))
308303simprd 495 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))
3093, 4, 5, 17, 18, 19, 271, 284, 287, 257, 267f1otrgds 28624 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑦𝐸𝑒) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘’)))
3103, 4, 5, 17, 18, 19, 271, 284, 287, 263, 269f1otrgds 28624 . . . . . . . . . . . . . . . . . 18 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑏𝐸𝑣) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘£)))
311308, 309, 3103eqtr3d 2774 . . . . . . . . . . . . . . . . 17 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘¦)𝐷(πΉβ€˜π‘’)) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘£)))
3123, 4, 5, 253, 256, 258, 260, 262, 264, 266, 268, 270, 280, 289, 292, 298, 302, 307, 311axtg5seg 28220 . . . . . . . . . . . . . . . 16 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ ((πΉβ€˜π‘§)𝐷(πΉβ€˜π‘’)) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘£)))
3133, 4, 5, 17, 18, 19, 271, 284, 287, 259, 267f1otrgds 28624 . . . . . . . . . . . . . . . 16 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑧𝐸𝑒) = ((πΉβ€˜π‘§)𝐷(πΉβ€˜π‘’)))
3143, 4, 5, 17, 18, 19, 271, 284, 287, 265, 269f1otrgds 28624 . . . . . . . . . . . . . . . 16 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑐𝐸𝑣) = ((πΉβ€˜π‘)𝐷(πΉβ€˜π‘£)))
315312, 313, 3143eqtr4d 2776 . . . . . . . . . . . . . . 15 ((((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ ((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣))))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣))
316315ex 412 . . . . . . . . . . . . . 14 (((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) β†’ (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
317316ralrimiva 3140 . . . . . . . . . . . . 13 ((((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) ∧ 𝑐 ∈ 𝐡) β†’ βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
318317ralrimiva 3140 . . . . . . . . . . . 12 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) ∧ 𝑏 ∈ 𝐡) β†’ βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
319318ralrimiva 3140 . . . . . . . . . . 11 ((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘Ž ∈ 𝐡) β†’ βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
320319ralrimiva 3140 . . . . . . . . . 10 (((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
321320ralrimiva 3140 . . . . . . . . 9 ((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
322321ralrimiva 3140 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑦 ∈ 𝐡) β†’ βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
323322ralrimiva 3140 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
324323ralrimiva 3140 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)))
325 simp-4l 780 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ πœ‘)
326 simplr 766 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝑀 ∈ 𝑃)
327 simprl 768 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀))
328325, 8syl 17 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝐹:𝐡–1-1-onto→𝑃)
329 f1ocnvfv2 7270 . . . . . . . . . . . . . 14 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑀 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘€)) = 𝑀)
330328, 326, 329syl2anc 583 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘€)) = 𝑀)
331330oveq2d 7420 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘€))) = ((πΉβ€˜π‘₯)𝐼𝑀))
332327, 331eleqtrrd 2830 . . . . . . . . . . 11 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘€))))
333325, 21sylan 579 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
334325, 23sylan 579 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
33512ad3antrrr 727 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ π‘₯ ∈ 𝐡)
33676ffvelcdmda 7079 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ 𝑃) β†’ (β—‘πΉβ€˜π‘€) ∈ 𝐡)
337325, 326, 336syl2anc 583 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (β—‘πΉβ€˜π‘€) ∈ 𝐡)
33814ad3antrrr 727 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝑦 ∈ 𝐡)
3393, 4, 5, 17, 18, 19, 328, 333, 334, 335, 337, 338f1otrgitv 28625 . . . . . . . . . . 11 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ↔ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘€)))))
340332, 339mpbird 257 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)))
3413, 4, 5, 17, 18, 19, 328, 333, 334, 338, 337f1otrgds 28624 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = ((πΉβ€˜π‘¦)𝐷(πΉβ€˜(β—‘πΉβ€˜π‘€))))
342330oveq2d 7420 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ ((πΉβ€˜π‘¦)𝐷(πΉβ€˜(β—‘πΉβ€˜π‘€))) = ((πΉβ€˜π‘¦)𝐷𝑀))
343 simprr 770 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
344341, 342, 3433eqtrd 2770 . . . . . . . . . . 11 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
345 simprl 768 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ π‘Ž ∈ 𝐡)
346345ad2antrr 723 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ π‘Ž ∈ 𝐡)
347 simprr 770 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ 𝑏 ∈ 𝐡)
348347ad2antrr 723 . . . . . . . . . . . 12 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ 𝑏 ∈ 𝐡)
3493, 4, 5, 17, 18, 19, 328, 333, 334, 346, 348f1otrgds 28624 . . . . . . . . . . 11 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (π‘ŽπΈπ‘) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))
350344, 349eqtr4d 2769 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘))
351 oveq2 7412 . . . . . . . . . . . . . . 15 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ (π‘₯𝐽𝑧) = (π‘₯𝐽(β—‘πΉβ€˜π‘€)))
352351eleq2d 2813 . . . . . . . . . . . . . 14 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ (𝑦 ∈ (π‘₯𝐽𝑧) ↔ 𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€))))
353 oveq2 7412 . . . . . . . . . . . . . . 15 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ (𝑦𝐸𝑧) = (𝑦𝐸(β—‘πΉβ€˜π‘€)))
354353eqeq1d 2728 . . . . . . . . . . . . . 14 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ ((𝑦𝐸𝑧) = (π‘ŽπΈπ‘) ↔ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘)))
355352, 354anbi12d 630 . . . . . . . . . . . . 13 (𝑧 = (β—‘πΉβ€˜π‘€) β†’ ((𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)) ↔ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ∧ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘))))
356355adantl 481 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀 ∈ 𝑃) ∧ 𝑧 = (β—‘πΉβ€˜π‘€)) β†’ ((𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)) ↔ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ∧ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘))))
357336, 356rspcedv 3599 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ 𝑃) β†’ ((𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ∧ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘)) β†’ βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘))))
358357imp 406 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ 𝑃) ∧ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘€)) ∧ (𝑦𝐸(β—‘πΉβ€˜π‘€)) = (π‘ŽπΈπ‘))) β†’ βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
359325, 326, 340, 350, 358syl22anc 836 . . . . . . . . 9 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) ∧ 𝑀 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘)))) β†’ βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
3607adantr 480 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ 𝐺 ∈ TarskiG)
36113adantr 480 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
36215adantr 480 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
36311adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
364363, 345ffvelcdmd 7080 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ (πΉβ€˜π‘Ž) ∈ 𝑃)
365363, 347ffvelcdmd 7080 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ (πΉβ€˜π‘) ∈ 𝑃)
3663, 4, 5, 360, 361, 362, 364, 365axtgsegcon 28219 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ βˆƒπ‘€ ∈ 𝑃 ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑀) ∧ ((πΉβ€˜π‘¦)𝐷𝑀) = ((πΉβ€˜π‘Ž)𝐷(πΉβ€˜π‘))))
367359, 366r19.29a 3156 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (π‘Ž ∈ 𝐡 ∧ 𝑏 ∈ 𝐡)) β†’ βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
368367ralrimivva 3194 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
369368ralrimivva 3194 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))
3702, 324, 369jca32 515 . . . . 5 (πœ‘ β†’ (𝐻 ∈ V ∧ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))))
37117, 18, 19istrkgcb 28211 . . . . 5 (𝐻 ∈ TarskiGCB ↔ (𝐻 ∈ V ∧ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐽𝑧) ∧ 𝑏 ∈ (π‘Žπ½π‘)) ∧ (((π‘₯𝐸𝑦) = (π‘ŽπΈπ‘) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((π‘₯𝐸𝑒) = (π‘ŽπΈπ‘£) ∧ (𝑦𝐸𝑒) = (𝑏𝐸𝑣)))) β†’ (𝑧𝐸𝑒) = (𝑐𝐸𝑣)) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (𝑦 ∈ (π‘₯𝐽𝑧) ∧ (𝑦𝐸𝑧) = (π‘ŽπΈπ‘)))))
372370, 371sylibr 233 . . . 4 (πœ‘ β†’ 𝐻 ∈ TarskiGCB)
373 f1otrg.l . . . . 5 (πœ‘ β†’ (LineGβ€˜π») = (π‘₯ ∈ 𝐡, 𝑦 ∈ (𝐡 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝐡 ∣ (𝑧 ∈ (π‘₯𝐽𝑦) ∨ π‘₯ ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (π‘₯𝐽𝑧))}))
37417, 18, 19istrkgl 28213 . . . . 5 (𝐻 ∈ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})} ↔ (𝐻 ∈ V ∧ (LineGβ€˜π») = (π‘₯ ∈ 𝐡, 𝑦 ∈ (𝐡 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝐡 ∣ (𝑧 ∈ (π‘₯𝐽𝑦) ∨ π‘₯ ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (π‘₯𝐽𝑧))})))
3752, 373, 374sylanbrc 582 . . . 4 (πœ‘ β†’ 𝐻 ∈ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})
376372, 375elind 4189 . . 3 (πœ‘ β†’ 𝐻 ∈ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
377252, 376elind 4189 . 2 (πœ‘ β†’ 𝐻 ∈ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})))
378 df-trkg 28208 . 2 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
379377, 378eleqtrrdi 2838 1 (πœ‘ β†’ 𝐻 ∈ TarskiG)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ w3o 1083   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  {cab 2703   β‰  wne 2934  βˆ€wral 3055  βˆƒwrex 3064  {crab 3426  Vcvv 3468  [wsbc 3772   βˆ– cdif 3940   ∩ cin 3942   βŠ† wss 3943  π’« cpw 4597  {csn 4623  β—‘ccnv 5668  ran crn 5670   β€œ cima 5672   Fn wfn 6531  βŸΆwf 6532  β€“1-1β†’wf1 6533  β€“ontoβ†’wfo 6534  β€“1-1-ontoβ†’wf1o 6535  β€˜cfv 6536  (class class class)co 7404   ∈ cmpo 7406  Basecbs 17151  distcds 17213  TarskiGcstrkg 28182  TarskiGCcstrkgc 28183  TarskiGBcstrkgb 28184  TarskiGCBcstrkgcb 28185  Itvcitv 28188  LineGclng 28189
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 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-sbc 3773  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7407  df-oprab 7408  df-mpo 7409  df-trkgc 28203  df-trkgb 28204  df-trkgcb 28205  df-trkg 28208
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator