MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1otrge Structured version   Visualization version   GIF version
Theorem f1otrge 28112
Description: A bijection between bases which conserves distances and intervals conserves also the property of being a Euclidean geometry. (Contributed by Thierry Arnoux, 23-Mar-2019.)
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 (πœ‘ β†’ 𝐻 ∈ 𝑉)
f1otrge.g (πœ‘ β†’ 𝐺 ∈ TarskiGE)
Assertion
Ref Expression
f1otrge (πœ‘ β†’ 𝐻 ∈ TarskiGE)
Distinct variable groups:   𝑒,𝑓,𝑔,𝐡   𝐷,𝑒,𝑓,𝑔   𝑒,𝐸,𝑓,𝑔   𝑒,𝐹,𝑓,𝑔   𝑒,𝐼,𝑓,𝑔   𝑒,𝐽,𝑓,𝑔   𝑃,𝑒,𝑓,𝑔   πœ‘,𝑒,𝑓,𝑔   𝑓,𝐻
Allowed substitution hints:   𝐺(𝑒,𝑓,𝑔)   𝐻(𝑒,𝑔)   𝑉(𝑒,𝑓,𝑔)
Proof of Theorem f1otrge
Dummy variables π‘Ž 𝑏 𝑐 𝑑 𝑒 𝑣 π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1otrg.h . . 3 (πœ‘ β†’ 𝐻 ∈ 𝑉)
21elexd 3494 . 2 (πœ‘ β†’ 𝐻 ∈ V)
3 f1otrkg.f . . . . . . . . . 10 (πœ‘ β†’ 𝐹:𝐡–1-1-onto→𝑃)
4 f1ocnv 6842 . . . . . . . . . 10 (𝐹:𝐡–1-1-onto→𝑃 β†’ ◑𝐹:𝑃–1-1-onto→𝐡)
5 f1of 6830 . . . . . . . . . 10 (◑𝐹:𝑃–1-1-onto→𝐡 β†’ ◑𝐹:π‘ƒβŸΆπ΅)
63, 4, 53syl 18 . . . . . . . . 9 (πœ‘ β†’ ◑𝐹:π‘ƒβŸΆπ΅)
76ad6antr 734 . . . . . . . 8 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ ◑𝐹:π‘ƒβŸΆπ΅)
8 simpllr 774 . . . . . . . 8 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ 𝑐 ∈ 𝑃)
97, 8ffvelcdmd 7084 . . . . . . 7 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ (β—‘πΉβ€˜π‘) ∈ 𝐡)
10 simplr 767 . . . . . . . 8 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ 𝑑 ∈ 𝑃)
117, 10ffvelcdmd 7084 . . . . . . 7 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ (β—‘πΉβ€˜π‘‘) ∈ 𝐡)
12 simpr1 1194 . . . . . . . . 9 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐))
133ad3antrrr 728 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ 𝐹:𝐡–1-1-onto→𝑃)
1413ad3antrrr 728 . . . . . . . . . . 11 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ 𝐹:𝐡–1-1-onto→𝑃)
15 f1ocnvfv2 7271 . . . . . . . . . . 11 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) = 𝑐)
1614, 8, 15syl2anc 584 . . . . . . . . . 10 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘)) = 𝑐)
1716oveq2d 7421 . . . . . . . . 9 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘))) = ((πΉβ€˜π‘₯)𝐼𝑐))
1812, 17eleqtrrd 2836 . . . . . . . 8 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘))))
19 f1otrkg.p . . . . . . . . 9 𝑃 = (Baseβ€˜πΊ)
20 f1otrkg.d . . . . . . . . 9 𝐷 = (distβ€˜πΊ)
21 f1otrkg.i . . . . . . . . 9 𝐼 = (Itvβ€˜πΊ)
22 f1otrkg.b . . . . . . . . 9 𝐡 = (Baseβ€˜π»)
23 f1otrkg.e . . . . . . . . 9 𝐸 = (distβ€˜π»)
24 f1otrkg.j . . . . . . . . 9 𝐽 = (Itvβ€˜π»)
25 f1otrkg.1 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
2625ad5ant15 757 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
2726ad5ant15 757 . . . . . . . . 9 ((((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡)) β†’ (𝑒𝐸𝑓) = ((πΉβ€˜π‘’)𝐷(πΉβ€˜π‘“)))
28 f1otrkg.2 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
2928ad5ant15 757 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
3029ad5ant15 757 . . . . . . . . 9 ((((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐡 ∧ 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡)) β†’ (𝑔 ∈ (𝑒𝐽𝑓) ↔ (πΉβ€˜π‘”) ∈ ((πΉβ€˜π‘’)𝐼(πΉβ€˜π‘“))))
31 simprl 769 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ π‘₯ ∈ 𝐡)
3231ad2antrr 724 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ π‘₯ ∈ 𝐡)
3332ad3antrrr 728 . . . . . . . . 9 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ π‘₯ ∈ 𝐡)
34 simprr 771 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ 𝑦 ∈ 𝐡)
3534ad2antrr 724 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ 𝑦 ∈ 𝐡)
3635ad3antrrr 728 . . . . . . . . 9 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ 𝑦 ∈ 𝐡)
3719, 20, 21, 22, 23, 24, 14, 27, 30, 33, 9, 36f1otrgitv 28110 . . . . . . . 8 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘)) ↔ (πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘)))))
3818, 37mpbird 256 . . . . . . 7 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ 𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘)))
39 simpr2 1195 . . . . . . . . 9 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑))
40 f1ocnvfv2 7271 . . . . . . . . . . 11 ((𝐹:𝐡–1-1-onto→𝑃 ∧ 𝑑 ∈ 𝑃) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘‘)) = 𝑑)
4114, 10, 40syl2anc 584 . . . . . . . . . 10 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘‘)) = 𝑑)
4241oveq2d 7421 . . . . . . . . 9 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘‘))) = ((πΉβ€˜π‘₯)𝐼𝑑))
4339, 42eleqtrrd 2836 . . . . . . . 8 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘‘))))
44 simplr1 1215 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ 𝑧 ∈ 𝐡)
4544ad3antrrr 728 . . . . . . . . 9 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ 𝑧 ∈ 𝐡)
4619, 20, 21, 22, 23, 24, 14, 27, 30, 33, 11, 45f1otrgitv 28110 . . . . . . . 8 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ (𝑧 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘‘)) ↔ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜(β—‘πΉβ€˜π‘‘)))))
4743, 46mpbird 256 . . . . . . 7 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ 𝑧 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘‘)))
48 simpr3 1196 . . . . . . . . 9 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))
4916, 41oveq12d 7423 . . . . . . . . 9 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ ((πΉβ€˜(β—‘πΉβ€˜π‘))𝐼(πΉβ€˜(β—‘πΉβ€˜π‘‘))) = (𝑐𝐼𝑑))
5048, 49eleqtrrd 2836 . . . . . . . 8 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ (πΉβ€˜π‘£) ∈ ((πΉβ€˜(β—‘πΉβ€˜π‘))𝐼(πΉβ€˜(β—‘πΉβ€˜π‘‘))))
51 simplr3 1217 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ 𝑣 ∈ 𝐡)
5251ad3antrrr 728 . . . . . . . . 9 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ 𝑣 ∈ 𝐡)
5319, 20, 21, 22, 23, 24, 14, 27, 30, 9, 11, 52f1otrgitv 28110 . . . . . . . 8 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ (𝑣 ∈ ((β—‘πΉβ€˜π‘)𝐽(β—‘πΉβ€˜π‘‘)) ↔ (πΉβ€˜π‘£) ∈ ((πΉβ€˜(β—‘πΉβ€˜π‘))𝐼(πΉβ€˜(β—‘πΉβ€˜π‘‘)))))
5450, 53mpbird 256 . . . . . . 7 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ 𝑣 ∈ ((β—‘πΉβ€˜π‘)𝐽(β—‘πΉβ€˜π‘‘)))
55 oveq2 7413 . . . . . . . . . 10 (π‘Ž = (β—‘πΉβ€˜π‘) β†’ (π‘₯π½π‘Ž) = (π‘₯𝐽(β—‘πΉβ€˜π‘)))
5655eleq2d 2819 . . . . . . . . 9 (π‘Ž = (β—‘πΉβ€˜π‘) β†’ (𝑦 ∈ (π‘₯π½π‘Ž) ↔ 𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘))))
57 oveq1 7412 . . . . . . . . . 10 (π‘Ž = (β—‘πΉβ€˜π‘) β†’ (π‘Žπ½π‘) = ((β—‘πΉβ€˜π‘)𝐽𝑏))
5857eleq2d 2819 . . . . . . . . 9 (π‘Ž = (β—‘πΉβ€˜π‘) β†’ (𝑣 ∈ (π‘Žπ½π‘) ↔ 𝑣 ∈ ((β—‘πΉβ€˜π‘)𝐽𝑏)))
5956, 583anbi13d 1438 . . . . . . . 8 (π‘Ž = (β—‘πΉβ€˜π‘) β†’ ((𝑦 ∈ (π‘₯π½π‘Ž) ∧ 𝑧 ∈ (π‘₯𝐽𝑏) ∧ 𝑣 ∈ (π‘Žπ½π‘)) ↔ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘)) ∧ 𝑧 ∈ (π‘₯𝐽𝑏) ∧ 𝑣 ∈ ((β—‘πΉβ€˜π‘)𝐽𝑏))))
60 oveq2 7413 . . . . . . . . . 10 (𝑏 = (β—‘πΉβ€˜π‘‘) β†’ (π‘₯𝐽𝑏) = (π‘₯𝐽(β—‘πΉβ€˜π‘‘)))
6160eleq2d 2819 . . . . . . . . 9 (𝑏 = (β—‘πΉβ€˜π‘‘) β†’ (𝑧 ∈ (π‘₯𝐽𝑏) ↔ 𝑧 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘‘))))
62 oveq2 7413 . . . . . . . . . 10 (𝑏 = (β—‘πΉβ€˜π‘‘) β†’ ((β—‘πΉβ€˜π‘)𝐽𝑏) = ((β—‘πΉβ€˜π‘)𝐽(β—‘πΉβ€˜π‘‘)))
6362eleq2d 2819 . . . . . . . . 9 (𝑏 = (β—‘πΉβ€˜π‘‘) β†’ (𝑣 ∈ ((β—‘πΉβ€˜π‘)𝐽𝑏) ↔ 𝑣 ∈ ((β—‘πΉβ€˜π‘)𝐽(β—‘πΉβ€˜π‘‘))))
6461, 633anbi23d 1439 . . . . . . . 8 (𝑏 = (β—‘πΉβ€˜π‘‘) β†’ ((𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘)) ∧ 𝑧 ∈ (π‘₯𝐽𝑏) ∧ 𝑣 ∈ ((β—‘πΉβ€˜π‘)𝐽𝑏)) ↔ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘)) ∧ 𝑧 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘‘)) ∧ 𝑣 ∈ ((β—‘πΉβ€˜π‘)𝐽(β—‘πΉβ€˜π‘‘)))))
6559, 64rspc2ev 3623 . . . . . . 7 (((β—‘πΉβ€˜π‘) ∈ 𝐡 ∧ (β—‘πΉβ€˜π‘‘) ∈ 𝐡 ∧ (𝑦 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘)) ∧ 𝑧 ∈ (π‘₯𝐽(β—‘πΉβ€˜π‘‘)) ∧ 𝑣 ∈ ((β—‘πΉβ€˜π‘)𝐽(β—‘πΉβ€˜π‘‘)))) β†’ βˆƒπ‘Ž ∈ 𝐡 βˆƒπ‘ ∈ 𝐡 (𝑦 ∈ (π‘₯π½π‘Ž) ∧ 𝑧 ∈ (π‘₯𝐽𝑏) ∧ 𝑣 ∈ (π‘Žπ½π‘)))
669, 11, 38, 47, 54, 65syl113anc 1382 . . . . . 6 (((((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑))) β†’ βˆƒπ‘Ž ∈ 𝐡 βˆƒπ‘ ∈ 𝐡 (𝑦 ∈ (π‘₯π½π‘Ž) ∧ 𝑧 ∈ (π‘₯𝐽𝑏) ∧ 𝑣 ∈ (π‘Žπ½π‘)))
67 f1otrge.g . . . . . . . 8 (πœ‘ β†’ 𝐺 ∈ TarskiGE)
6867ad3antrrr 728 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ 𝐺 ∈ TarskiGE)
69 f1of 6830 . . . . . . . . . . 11 (𝐹:𝐡–1-1-onto→𝑃 β†’ 𝐹:π΅βŸΆπ‘ƒ)
703, 69syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:π΅βŸΆπ‘ƒ)
7170adantr 481 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
7271, 31ffvelcdmd 7084 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
7372ad2antrr 724 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ (πΉβ€˜π‘₯) ∈ 𝑃)
7471, 34ffvelcdmd 7084 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
7574ad2antrr 724 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ (πΉβ€˜π‘¦) ∈ 𝑃)
7670ad3antrrr 728 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ 𝐹:π΅βŸΆπ‘ƒ)
7776, 44ffvelcdmd 7084 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ (πΉβ€˜π‘§) ∈ 𝑃)
78 simplr2 1216 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ 𝑒 ∈ 𝐡)
7976, 78ffvelcdmd 7084 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ (πΉβ€˜π‘’) ∈ 𝑃)
8076, 51ffvelcdmd 7084 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ (πΉβ€˜π‘£) ∈ 𝑃)
81 simpr1 1194 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ 𝑒 ∈ (π‘₯𝐽𝑣))
8219, 20, 21, 22, 23, 24, 13, 26, 29, 32, 51, 78f1otrgitv 28110 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ (𝑒 ∈ (π‘₯𝐽𝑣) ↔ (πΉβ€˜π‘’) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘£))))
8381, 82mpbid 231 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ (πΉβ€˜π‘’) ∈ ((πΉβ€˜π‘₯)𝐼(πΉβ€˜π‘£)))
84 simpr2 1195 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ 𝑒 ∈ (𝑦𝐽𝑧))
8519, 20, 21, 22, 23, 24, 13, 26, 29, 35, 44, 78f1otrgitv 28110 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ (𝑒 ∈ (𝑦𝐽𝑧) ↔ (πΉβ€˜π‘’) ∈ ((πΉβ€˜π‘¦)𝐼(πΉβ€˜π‘§))))
8684, 85mpbid 231 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ (πΉβ€˜π‘’) ∈ ((πΉβ€˜π‘¦)𝐼(πΉβ€˜π‘§)))
87 simpr3 1196 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ π‘₯ β‰  𝑒)
88 dff1o6 7269 . . . . . . . . . . . . 13 (𝐹:𝐡–1-1-onto→𝑃 ↔ (𝐹 Fn 𝐡 ∧ ran 𝐹 = 𝑃 ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 ((πΉβ€˜π‘₯) = (πΉβ€˜π‘’) β†’ π‘₯ = 𝑒)))
8988simp3bi 1147 . . . . . . . . . . . 12 (𝐹:𝐡–1-1-onto→𝑃 β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 ((πΉβ€˜π‘₯) = (πΉβ€˜π‘’) β†’ π‘₯ = 𝑒))
9089r19.21bi 3248 . . . . . . . . . . 11 ((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘’ ∈ 𝐡 ((πΉβ€˜π‘₯) = (πΉβ€˜π‘’) β†’ π‘₯ = 𝑒))
9190r19.21bi 3248 . . . . . . . . . 10 (((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ ((πΉβ€˜π‘₯) = (πΉβ€˜π‘’) β†’ π‘₯ = 𝑒))
9291necon3d 2961 . . . . . . . . 9 (((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ (π‘₯ β‰  𝑒 β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘’)))
9392imp 407 . . . . . . . 8 ((((𝐹:𝐡–1-1-onto→𝑃 ∧ π‘₯ ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) ∧ π‘₯ β‰  𝑒) β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘’))
9413, 32, 78, 87, 93syl1111anc 838 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘’))
9519, 20, 21, 68, 73, 75, 77, 79, 80, 83, 86, 94axtgeucl 27712 . . . . . 6 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 ((πΉβ€˜π‘¦) ∈ ((πΉβ€˜π‘₯)𝐼𝑐) ∧ (πΉβ€˜π‘§) ∈ ((πΉβ€˜π‘₯)𝐼𝑑) ∧ (πΉβ€˜π‘£) ∈ (𝑐𝐼𝑑)))
9666, 95r19.29vva 3213 . . . . 5 ((((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) ∧ (𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒)) β†’ βˆƒπ‘Ž ∈ 𝐡 βˆƒπ‘ ∈ 𝐡 (𝑦 ∈ (π‘₯π½π‘Ž) ∧ 𝑧 ∈ (π‘₯𝐽𝑏) ∧ 𝑣 ∈ (π‘Žπ½π‘)))
9796ex 413 . . . 4 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) ∧ (𝑧 ∈ 𝐡 ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) β†’ ((𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒) β†’ βˆƒπ‘Ž ∈ 𝐡 βˆƒπ‘ ∈ 𝐡 (𝑦 ∈ (π‘₯π½π‘Ž) ∧ 𝑧 ∈ (π‘₯𝐽𝑏) ∧ 𝑣 ∈ (π‘Žπ½π‘))))
9897ralrimivvva 3203 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒) β†’ βˆƒπ‘Ž ∈ 𝐡 βˆƒπ‘ ∈ 𝐡 (𝑦 ∈ (π‘₯π½π‘Ž) ∧ 𝑧 ∈ (π‘₯𝐽𝑏) ∧ 𝑣 ∈ (π‘Žπ½π‘))))
9998ralrimivva 3200 . 2 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒) β†’ βˆƒπ‘Ž ∈ 𝐡 βˆƒπ‘ ∈ 𝐡 (𝑦 ∈ (π‘₯π½π‘Ž) ∧ 𝑧 ∈ (π‘₯𝐽𝑏) ∧ 𝑣 ∈ (π‘Žπ½π‘))))
10022, 23, 24istrkge 27697 . 2 (𝐻 ∈ TarskiGE ↔ (𝐻 ∈ V ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 ((𝑒 ∈ (π‘₯𝐽𝑣) ∧ 𝑒 ∈ (𝑦𝐽𝑧) ∧ π‘₯ β‰  𝑒) β†’ βˆƒπ‘Ž ∈ 𝐡 βˆƒπ‘ ∈ 𝐡 (𝑦 ∈ (π‘₯π½π‘Ž) ∧ 𝑧 ∈ (π‘₯𝐽𝑏) ∧ 𝑣 ∈ (π‘Žπ½π‘)))))
1012, 99, 100sylanbrc 583 1 (πœ‘ β†’ 𝐻 ∈ TarskiGE)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474  β—‘ccnv 5674  ran crn 5676   Fn wfn 6535  βŸΆwf 6536  β€“1-1-ontoβ†’wf1o 6539  β€˜cfv 6540  (class class class)co 7405  Basecbs 17140  distcds 17202  TarskiGEcstrkge 27672  Itvcitv 27673
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-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-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-trkge 27691
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator