Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  afsval Structured version   Visualization version   GIF version

Theorem afsval 34147
Description: Value of the AFS relation for a given geometry structure. (Contributed by Thierry Arnoux, 20-Mar-2019.)
Hypotheses
Ref Expression
brafs.p 𝑃 = (Baseβ€˜πΊ)
brafs.d βˆ’ = (distβ€˜πΊ)
brafs.i 𝐼 = (Itvβ€˜πΊ)
brafs.g (πœ‘ β†’ 𝐺 ∈ TarskiG)
Assertion
Ref Expression
afsval (πœ‘ β†’ (AFSβ€˜πΊ) = {βŸ¨π‘’, π‘“βŸ© ∣ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀))))})
Distinct variable groups:   𝑒,𝑓,𝐺   π‘Ž,𝑏,𝑐,𝑑,𝑀,π‘₯,𝑦,𝑧,𝐼   𝑒,π‘Ž,𝑓,𝑃,𝑏,𝑐,𝑑,𝑀,π‘₯,𝑦,𝑧   βˆ’ ,π‘Ž,𝑏,𝑐,𝑑,𝑀,π‘₯,𝑦,𝑧   πœ‘,𝑒,𝑓
Allowed substitution hints:   πœ‘(π‘₯,𝑦,𝑧,𝑀,π‘Ž,𝑏,𝑐,𝑑)   𝐺(π‘₯,𝑦,𝑧,𝑀,π‘Ž,𝑏,𝑐,𝑑)   𝐼(𝑒,𝑓)   βˆ’ (𝑒,𝑓)

Proof of Theorem afsval
Dummy variables 𝑔 β„Ž 𝑖 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-afs 34146 . . 3 AFS = (𝑔 ∈ TarskiG ↦ {βŸ¨π‘’, π‘“βŸ© ∣ [(Baseβ€˜π‘”) / 𝑝][(distβ€˜π‘”) / β„Ž][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘Ž ∈ 𝑝 βˆƒπ‘ ∈ 𝑝 βˆƒπ‘ ∈ 𝑝 βˆƒπ‘‘ ∈ 𝑝 βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 βˆƒπ‘€ ∈ 𝑝 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€))))})
21a1i 11 . 2 (πœ‘ β†’ AFS = (𝑔 ∈ TarskiG ↦ {βŸ¨π‘’, π‘“βŸ© ∣ [(Baseβ€˜π‘”) / 𝑝][(distβ€˜π‘”) / β„Ž][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘Ž ∈ 𝑝 βˆƒπ‘ ∈ 𝑝 βˆƒπ‘ ∈ 𝑝 βˆƒπ‘‘ ∈ 𝑝 βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 βˆƒπ‘€ ∈ 𝑝 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€))))}))
3 brafs.p . . . . 5 𝑃 = (Baseβ€˜πΊ)
4 brafs.d . . . . 5 βˆ’ = (distβ€˜πΊ)
5 brafs.i . . . . 5 𝐼 = (Itvβ€˜πΊ)
6 simp1 1135 . . . . . . 7 ((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) β†’ 𝑝 = 𝑃)
76eqcomd 2737 . . . . . 6 ((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) β†’ 𝑃 = 𝑝)
87adantr 480 . . . . . . 7 (((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) β†’ 𝑃 = 𝑝)
98adantr 480 . . . . . . . 8 ((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) β†’ 𝑃 = 𝑝)
109adantr 480 . . . . . . . . 9 (((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) β†’ 𝑃 = 𝑝)
1110adantr 480 . . . . . . . . . 10 ((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) β†’ 𝑃 = 𝑝)
1211adantr 480 . . . . . . . . . . 11 (((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) β†’ 𝑃 = 𝑝)
1312adantr 480 . . . . . . . . . . . 12 ((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) β†’ 𝑃 = 𝑝)
147ad7antr 735 . . . . . . . . . . . . 13 (((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) β†’ 𝑃 = 𝑝)
15 simp3 1137 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) β†’ 𝑖 = 𝐼)
1615ad8antr 737 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ 𝑖 = 𝐼)
1716eqcomd 2737 . . . . . . . . . . . . . . . . . 18 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ 𝐼 = 𝑖)
1817oveqd 7429 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (π‘ŽπΌπ‘) = (π‘Žπ‘–π‘))
1918eleq2d 2818 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (𝑏 ∈ (π‘ŽπΌπ‘) ↔ 𝑏 ∈ (π‘Žπ‘–π‘)))
2017oveqd 7429 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (π‘₯𝐼𝑧) = (π‘₯𝑖𝑧))
2120eleq2d 2818 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (𝑦 ∈ (π‘₯𝐼𝑧) ↔ 𝑦 ∈ (π‘₯𝑖𝑧)))
2219, 21anbi12d 630 . . . . . . . . . . . . . . 15 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ↔ (𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧))))
23 simp2 1136 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) β†’ β„Ž = βˆ’ )
2423eqcomd 2737 . . . . . . . . . . . . . . . . . . 19 ((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) β†’ βˆ’ = β„Ž)
2524ad8antr 737 . . . . . . . . . . . . . . . . . 18 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ βˆ’ = β„Ž)
2625oveqd 7429 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (π‘Ž βˆ’ 𝑏) = (π‘Žβ„Žπ‘))
2725oveqd 7429 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (π‘₯ βˆ’ 𝑦) = (π‘₯β„Žπ‘¦))
2826, 27eqeq12d 2747 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ↔ (π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦)))
2925oveqd 7429 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (𝑏 βˆ’ 𝑐) = (π‘β„Žπ‘))
3025oveqd 7429 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (𝑦 βˆ’ 𝑧) = (π‘¦β„Žπ‘§))
3129, 30eqeq12d 2747 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ ((𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧) ↔ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)))
3228, 31anbi12d 630 . . . . . . . . . . . . . . 15 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ↔ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§))))
3325oveqd 7429 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (π‘Ž βˆ’ 𝑑) = (π‘Žβ„Žπ‘‘))
3425oveqd 7429 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (π‘₯ βˆ’ 𝑀) = (π‘₯β„Žπ‘€))
3533, 34eqeq12d 2747 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ↔ (π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€)))
3625oveqd 7429 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (𝑏 βˆ’ 𝑑) = (π‘β„Žπ‘‘))
3725oveqd 7429 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (𝑦 βˆ’ 𝑀) = (π‘¦β„Žπ‘€))
3836, 37eqeq12d 2747 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ ((𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀) ↔ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€)))
3935, 38anbi12d 630 . . . . . . . . . . . . . . 15 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)) ↔ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€))))
4022, 32, 393anbi123d 1435 . . . . . . . . . . . . . 14 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ (((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀))) ↔ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€)))))
41403anbi3d 1441 . . . . . . . . . . . . 13 ((((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) β†’ ((𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) ↔ (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€))))))
4214, 41rexeqbidva 3327 . . . . . . . . . . . 12 (((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) β†’ (βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) ↔ βˆƒπ‘€ ∈ 𝑝 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€))))))
4313, 42rexeqbidva 3327 . . . . . . . . . . 11 ((((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) β†’ (βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) ↔ βˆƒπ‘§ ∈ 𝑝 βˆƒπ‘€ ∈ 𝑝 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€))))))
4412, 43rexeqbidva 3327 . . . . . . . . . 10 (((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) β†’ (βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) ↔ βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 βˆƒπ‘€ ∈ 𝑝 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€))))))
4511, 44rexeqbidva 3327 . . . . . . . . 9 ((((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) β†’ (βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) ↔ βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 βˆƒπ‘€ ∈ 𝑝 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€))))))
4610, 45rexeqbidva 3327 . . . . . . . 8 (((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) β†’ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) ↔ βˆƒπ‘‘ ∈ 𝑝 βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 βˆƒπ‘€ ∈ 𝑝 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€))))))
479, 46rexeqbidva 3327 . . . . . . 7 ((((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) ∧ 𝑏 ∈ 𝑃) β†’ (βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) ↔ βˆƒπ‘ ∈ 𝑝 βˆƒπ‘‘ ∈ 𝑝 βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 βˆƒπ‘€ ∈ 𝑝 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€))))))
488, 47rexeqbidva 3327 . . . . . 6 (((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) ∧ π‘Ž ∈ 𝑃) β†’ (βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) ↔ βˆƒπ‘ ∈ 𝑝 βˆƒπ‘ ∈ 𝑝 βˆƒπ‘‘ ∈ 𝑝 βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 βˆƒπ‘€ ∈ 𝑝 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€))))))
497, 48rexeqbidva 3327 . . . . 5 ((𝑝 = 𝑃 ∧ β„Ž = βˆ’ ∧ 𝑖 = 𝐼) β†’ (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) ↔ βˆƒπ‘Ž ∈ 𝑝 βˆƒπ‘ ∈ 𝑝 βˆƒπ‘ ∈ 𝑝 βˆƒπ‘‘ ∈ 𝑝 βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 βˆƒπ‘€ ∈ 𝑝 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€))))))
503, 4, 5, 49sbcie3s 17102 . . . 4 (𝑔 = 𝐺 β†’ ([(Baseβ€˜π‘”) / 𝑝][(distβ€˜π‘”) / β„Ž][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘Ž ∈ 𝑝 βˆƒπ‘ ∈ 𝑝 βˆƒπ‘ ∈ 𝑝 βˆƒπ‘‘ ∈ 𝑝 βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 βˆƒπ‘€ ∈ 𝑝 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€)))) ↔ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀))))))
5150adantl 481 . . 3 ((πœ‘ ∧ 𝑔 = 𝐺) β†’ ([(Baseβ€˜π‘”) / 𝑝][(distβ€˜π‘”) / β„Ž][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘Ž ∈ 𝑝 βˆƒπ‘ ∈ 𝑝 βˆƒπ‘ ∈ 𝑝 βˆƒπ‘‘ ∈ 𝑝 βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 βˆƒπ‘€ ∈ 𝑝 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€)))) ↔ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀))))))
5251opabbidv 5214 . 2 ((πœ‘ ∧ 𝑔 = 𝐺) β†’ {βŸ¨π‘’, π‘“βŸ© ∣ [(Baseβ€˜π‘”) / 𝑝][(distβ€˜π‘”) / β„Ž][(Itvβ€˜π‘”) / 𝑖]βˆƒπ‘Ž ∈ 𝑝 βˆƒπ‘ ∈ 𝑝 βˆƒπ‘ ∈ 𝑝 βˆƒπ‘‘ ∈ 𝑝 βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 βˆƒπ‘€ ∈ 𝑝 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘Žπ‘–π‘) ∧ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ ((π‘Žβ„Žπ‘) = (π‘₯β„Žπ‘¦) ∧ (π‘β„Žπ‘) = (π‘¦β„Žπ‘§)) ∧ ((π‘Žβ„Žπ‘‘) = (π‘₯β„Žπ‘€) ∧ (π‘β„Žπ‘‘) = (π‘¦β„Žπ‘€))))} = {βŸ¨π‘’, π‘“βŸ© ∣ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀))))})
53 brafs.g . 2 (πœ‘ β†’ 𝐺 ∈ TarskiG)
54 df-xp 5682 . . . . 5 (((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) Γ— ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃))) = {βŸ¨π‘’, π‘“βŸ© ∣ (𝑒 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) ∧ 𝑓 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))}
553fvexi 6905 . . . . . . . 8 𝑃 ∈ V
5655, 55xpex 7744 . . . . . . 7 (𝑃 Γ— 𝑃) ∈ V
5756, 56xpex 7744 . . . . . 6 ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) ∈ V
5857, 57xpex 7744 . . . . 5 (((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) Γ— ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃))) ∈ V
5954, 58eqeltrri 2829 . . . 4 {βŸ¨π‘’, π‘“βŸ© ∣ (𝑒 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) ∧ 𝑓 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))} ∈ V
60 3simpa 1147 . . . . . . . . . . . . . 14 ((𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) β†’ (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©))
6160reximi 3083 . . . . . . . . . . . . 13 (βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) β†’ βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©))
6261reximi 3083 . . . . . . . . . . . 12 (βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) β†’ βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©))
6362reximi 3083 . . . . . . . . . . 11 (βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) β†’ βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©))
6463reximi 3083 . . . . . . . . . 10 (βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) β†’ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©))
6564reximi 3083 . . . . . . . . 9 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) β†’ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©))
6665reximi 3083 . . . . . . . 8 (βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) β†’ βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©))
6766reximi 3083 . . . . . . 7 (βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) β†’ βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©))
6867reximi 3083 . . . . . 6 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©))
69 simpr 484 . . . . . . . . . . . . . . 15 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ©) β†’ 𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ©)
70 opelxpi 5713 . . . . . . . . . . . . . . . . 17 ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ (𝑃 Γ— 𝑃))
7170ad7antr 735 . . . . . . . . . . . . . . . 16 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ©) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ (𝑃 Γ— 𝑃))
72 simp-7r 787 . . . . . . . . . . . . . . . . 17 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ©) β†’ 𝑐 ∈ 𝑃)
73 simp-6r 785 . . . . . . . . . . . . . . . . 17 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ©) β†’ 𝑑 ∈ 𝑃)
74 opelxpi 5713 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) β†’ βŸ¨π‘, π‘‘βŸ© ∈ (𝑃 Γ— 𝑃))
7572, 73, 74syl2anc 583 . . . . . . . . . . . . . . . 16 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ©) β†’ βŸ¨π‘, π‘‘βŸ© ∈ (𝑃 Γ— 𝑃))
76 opelxpi 5713 . . . . . . . . . . . . . . . 16 ((βŸ¨π‘Ž, π‘βŸ© ∈ (𝑃 Γ— 𝑃) ∧ βŸ¨π‘, π‘‘βŸ© ∈ (𝑃 Γ— 𝑃)) β†’ βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))
7771, 75, 76syl2anc 583 . . . . . . . . . . . . . . 15 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ©) β†’ βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))
7869, 77eqeltrd 2832 . . . . . . . . . . . . . 14 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ©) β†’ 𝑒 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))
79 simpr 484 . . . . . . . . . . . . . . 15 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©)
80 simp-5r 783 . . . . . . . . . . . . . . . . 17 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ π‘₯ ∈ 𝑃)
81 simp-4r 781 . . . . . . . . . . . . . . . . 17 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ 𝑦 ∈ 𝑃)
82 opelxpi 5713 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) β†’ ⟨π‘₯, π‘¦βŸ© ∈ (𝑃 Γ— 𝑃))
8380, 81, 82syl2anc 583 . . . . . . . . . . . . . . . 16 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ ⟨π‘₯, π‘¦βŸ© ∈ (𝑃 Γ— 𝑃))
84 simpllr 773 . . . . . . . . . . . . . . . . 17 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ 𝑧 ∈ 𝑃)
85 simplr 766 . . . . . . . . . . . . . . . . 17 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ 𝑀 ∈ 𝑃)
86 opelxpi 5713 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ 𝑃 ∧ 𝑀 ∈ 𝑃) β†’ βŸ¨π‘§, π‘€βŸ© ∈ (𝑃 Γ— 𝑃))
8784, 85, 86syl2anc 583 . . . . . . . . . . . . . . . 16 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ βŸ¨π‘§, π‘€βŸ© ∈ (𝑃 Γ— 𝑃))
88 opelxpi 5713 . . . . . . . . . . . . . . . 16 ((⟨π‘₯, π‘¦βŸ© ∈ (𝑃 Γ— 𝑃) ∧ βŸ¨π‘§, π‘€βŸ© ∈ (𝑃 Γ— 𝑃)) β†’ ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))
8983, 87, 88syl2anc 583 . . . . . . . . . . . . . . 15 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))
9079, 89eqeltrd 2832 . . . . . . . . . . . . . 14 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ 𝑓 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))
9178, 90anim12dan 618 . . . . . . . . . . . . 13 (((((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑀 ∈ 𝑃) ∧ (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©)) β†’ (𝑒 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) ∧ 𝑓 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃))))
9291rexlimdva2 3156 . . . . . . . . . . . 12 (((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) β†’ (βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ (𝑒 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) ∧ 𝑓 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))))
9392rexlimdva 3154 . . . . . . . . . . 11 ((((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) β†’ (βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ (𝑒 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) ∧ 𝑓 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))))
9493rexlimdva 3154 . . . . . . . . . 10 (((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ π‘₯ ∈ 𝑃) β†’ (βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ (𝑒 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) ∧ 𝑓 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))))
9594rexlimdva 3154 . . . . . . . . 9 ((((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) β†’ (βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ (𝑒 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) ∧ 𝑓 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))))
9695rexlimdva 3154 . . . . . . . 8 (((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) β†’ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ (𝑒 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) ∧ 𝑓 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))))
9796rexlimdva 3154 . . . . . . 7 ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) β†’ (βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ (𝑒 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) ∧ 𝑓 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))))
9897rexlimivv 3198 . . . . . 6 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ©) β†’ (𝑒 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) ∧ 𝑓 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃))))
9968, 98syl 17 . . . . 5 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀)))) β†’ (𝑒 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) ∧ 𝑓 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃))))
10099ssopab2i 5550 . . . 4 {βŸ¨π‘’, π‘“βŸ© ∣ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀))))} βŠ† {βŸ¨π‘’, π‘“βŸ© ∣ (𝑒 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)) ∧ 𝑓 ∈ ((𝑃 Γ— 𝑃) Γ— (𝑃 Γ— 𝑃)))}
10159, 100ssexi 5322 . . 3 {βŸ¨π‘’, π‘“βŸ© ∣ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀))))} ∈ V
102101a1i 11 . 2 (πœ‘ β†’ {βŸ¨π‘’, π‘“βŸ© ∣ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀))))} ∈ V)
1032, 52, 53, 102fvmptd 7005 1 (πœ‘ β†’ (AFSβ€˜πΊ) = {βŸ¨π‘’, π‘“βŸ© ∣ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘€ ∈ 𝑃 (𝑒 = βŸ¨βŸ¨π‘Ž, π‘βŸ©, βŸ¨π‘, π‘‘βŸ©βŸ© ∧ 𝑓 = ⟨⟨π‘₯, π‘¦βŸ©, βŸ¨π‘§, π‘€βŸ©βŸ© ∧ ((𝑏 ∈ (π‘ŽπΌπ‘) ∧ 𝑦 ∈ (π‘₯𝐼𝑧)) ∧ ((π‘Ž βˆ’ 𝑏) = (π‘₯ βˆ’ 𝑦) ∧ (𝑏 βˆ’ 𝑐) = (𝑦 βˆ’ 𝑧)) ∧ ((π‘Ž βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑀) ∧ (𝑏 βˆ’ 𝑑) = (𝑦 βˆ’ 𝑀))))})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  βˆƒwrex 3069  Vcvv 3473  [wsbc 3777  βŸ¨cop 4634  {copab 5210   ↦ cmpt 5231   Γ— cxp 5674  β€˜cfv 6543  (class class class)co 7412  Basecbs 17151  distcds 17213  TarskiGcstrkg 28111  Itvcitv 28117  AFScafs 34145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7415  df-afs 34146
This theorem is referenced by:  brafs  34148
  Copyright terms: Public domain W3C validator