Metamath Proof Explorer

Theorem afsval

Description: Value of the AFS relation for a given geometry structure. (Contributed by Thierry Arnoux, 20-Mar-2019)

Ref Expression
Hypotheses brafs.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
brafs.d ⊢ − = ( dist ‘ 𝐺 )
brafs.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
brafs.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
Assertion afsval ( 𝜑 → ( AFS ‘ 𝐺 ) = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 brafs.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 brafs.d ⊢ − = ( dist ‘ 𝐺 )
3 brafs.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 brafs.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 df-afs ⊢ AFS = ( 𝑔 ∈ TarskiG ↦ { ⟨ 𝑒 , 𝑓 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / ℎ ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ∃ 𝑐 ∈ 𝑝 ∃ 𝑑 ∈ 𝑝 ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ∃ 𝑤 ∈ 𝑝 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) } )
6 5 a1i ⊢ ( 𝜑 → AFS = ( 𝑔 ∈ TarskiG ↦ { ⟨ 𝑒 , 𝑓 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / ℎ ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ∃ 𝑐 ∈ 𝑝 ∃ 𝑑 ∈ 𝑝 ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ∃ 𝑤 ∈ 𝑝 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) } ) )
7 simp1 ⊢ ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) → 𝑝 = 𝑃 )
8 7 eqcomd ⊢ ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) → 𝑃 = 𝑝 )
9 8 adantr ⊢ ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) → 𝑃 = 𝑝 )
10 9 adantr ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → 𝑃 = 𝑝 )
11 10 adantr ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) → 𝑃 = 𝑝 )
12 11 adantr ⊢ ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) → 𝑃 = 𝑝 )
13 12 adantr ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) → 𝑃 = 𝑝 )
14 13 adantr ⊢ ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → 𝑃 = 𝑝 )
15 8 ad7antr ⊢ ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → 𝑃 = 𝑝 )
16 simp3 ⊢ ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) → 𝑖 = 𝐼 )
17 16 ad8antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → 𝑖 = 𝐼 )
18 17 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → 𝐼 = 𝑖 )
19 18 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( 𝑎 𝐼 𝑐 ) = ( 𝑎 𝑖 𝑐 ) )
20 19 eleq2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ↔ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) )
21 18 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( 𝑥 𝐼 𝑧 ) = ( 𝑥 𝑖 𝑧 ) )
22 21 eleq2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
23 20 22 anbi12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) )
24 simp2 ⊢ ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) → ℎ = − )
25 24 eqcomd ⊢ ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) → − = ℎ )
26 25 ad8antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → − = ℎ )
27 26 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( 𝑎 − 𝑏 ) = ( 𝑎 ℎ 𝑏 ) )
28 26 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( 𝑥 − 𝑦 ) = ( 𝑥 ℎ 𝑦 ) )
29 27 28 eqeq12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ↔ ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ) )
30 26 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( 𝑏 − 𝑐 ) = ( 𝑏 ℎ 𝑐 ) )
31 26 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( 𝑦 − 𝑧 ) = ( 𝑦 ℎ 𝑧 ) )
32 30 31 eqeq12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ↔ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) )
33 29 32 anbi12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ↔ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ) )
34 26 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( 𝑎 − 𝑑 ) = ( 𝑎 ℎ 𝑑 ) )
35 26 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( 𝑥 − 𝑤 ) = ( 𝑥 ℎ 𝑤 ) )
36 34 35 eqeq12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ↔ ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ) )
37 26 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( 𝑏 − 𝑑 ) = ( 𝑏 ℎ 𝑑 ) )
38 26 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( 𝑦 − 𝑤 ) = ( 𝑦 ℎ 𝑤 ) )
39 37 38 eqeq12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ↔ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) )
40 36 39 anbi12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ↔ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) )
41 23 33 40 3anbi123d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ↔ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) )
42 41 3anbi3d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → ( ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) ↔ ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) ) )
43 15 42 rexeqbidva ⊢ ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) ↔ ∃ 𝑤 ∈ 𝑝 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) ) )
44 14 43 rexeqbidva ⊢ ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) ↔ ∃ 𝑧 ∈ 𝑝 ∃ 𝑤 ∈ 𝑝 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) ) )
45 13 44 rexeqbidva ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) → ( ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) ↔ ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ∃ 𝑤 ∈ 𝑝 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) ) )
46 12 45 rexeqbidva ⊢ ( ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) ↔ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ∃ 𝑤 ∈ 𝑝 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) ) )
47 11 46 rexeqbidva ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) ↔ ∃ 𝑑 ∈ 𝑝 ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ∃ 𝑤 ∈ 𝑝 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) ) )
48 10 47 rexeqbidva ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) ↔ ∃ 𝑐 ∈ 𝑝 ∃ 𝑑 ∈ 𝑝 ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ∃ 𝑤 ∈ 𝑝 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) ) )
49 9 48 rexeqbidva ⊢ ( ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) ∧ 𝑎 ∈ 𝑃 ) → ( ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) ↔ ∃ 𝑏 ∈ 𝑝 ∃ 𝑐 ∈ 𝑝 ∃ 𝑑 ∈ 𝑝 ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ∃ 𝑤 ∈ 𝑝 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) ) )
50 8 49 rexeqbidva ⊢ ( ( 𝑝 = 𝑃 ∧ ℎ = − ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) ↔ ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ∃ 𝑐 ∈ 𝑝 ∃ 𝑑 ∈ 𝑝 ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ∃ 𝑤 ∈ 𝑝 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) ) )
51 1 2 3 50 sbcie3s ⊢ ( 𝑔 = 𝐺 → ( [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / ℎ ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ∃ 𝑐 ∈ 𝑝 ∃ 𝑑 ∈ 𝑝 ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ∃ 𝑤 ∈ 𝑝 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) ) )
52 51 adantl ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / ℎ ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ∃ 𝑐 ∈ 𝑝 ∃ 𝑑 ∈ 𝑝 ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ∃ 𝑤 ∈ 𝑝 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) ) )
53 52 opabbidv ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → { ⟨ 𝑒 , 𝑓 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / ℎ ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ∃ 𝑐 ∈ 𝑝 ∃ 𝑑 ∈ 𝑝 ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ∃ 𝑤 ∈ 𝑝 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑏 ) = ( 𝑥 ℎ 𝑦 ) ∧ ( 𝑏 ℎ 𝑐 ) = ( 𝑦 ℎ 𝑧 ) ) ∧ ( ( 𝑎 ℎ 𝑑 ) = ( 𝑥 ℎ 𝑤 ) ∧ ( 𝑏 ℎ 𝑑 ) = ( 𝑦 ℎ 𝑤 ) ) ) ) } = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) } )
54 df-xp ⊢ ( ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) × ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ∧ 𝑓 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) }
55 1 fvexi ⊢ 𝑃 ∈ V
56 55 55 xpex ⊢ ( 𝑃 × 𝑃 ) ∈ V
57 56 56 xpex ⊢ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ∈ V
58 57 57 xpex ⊢ ( ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) × ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) ∈ V
59 54 58 eqeltrri ⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ∧ 𝑓 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) } ∈ V
60 3simpa ⊢ ( ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) → ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) )
61 60 reximi ⊢ ( ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) → ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) )
62 61 reximi ⊢ ( ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) → ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) )
63 62 reximi ⊢ ( ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) → ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) )
64 63 reximi ⊢ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) )
65 64 reximi ⊢ ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) → ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) )
66 65 reximi ⊢ ( ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) → ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) )
67 66 reximi ⊢ ( ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) → ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) )
68 67 reximi ⊢ ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) )
69 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ) → 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ )
70 opelxpi ⊢ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑃 × 𝑃 ) )
71 70 ad7antr ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑃 × 𝑃 ) )
72 simp-7r ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ) → 𝑐 ∈ 𝑃 )
73 simp-6r ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ) → 𝑑 ∈ 𝑃 )
74 opelxpi ⊢ ( ( 𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃 ) → ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝑃 × 𝑃 ) )
75 72 73 74 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ) → ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝑃 × 𝑃 ) )
76 opelxpi ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑃 × 𝑃 ) ∧ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝑃 × 𝑃 ) ) → ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) )
77 71 75 76 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ) → ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) )
78 69 77 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ) → 𝑒 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) )
79 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ )
80 simp-5r ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → 𝑥 ∈ 𝑃 )
81 simp-4r ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → 𝑦 ∈ 𝑃 )
82 opelxpi ⊢ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑃 × 𝑃 ) )
83 80 81 82 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑃 × 𝑃 ) )
84 simpllr ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → 𝑧 ∈ 𝑃 )
85 simplr ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → 𝑤 ∈ 𝑃 )
86 opelxpi ⊢ ( ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝑃 ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑃 × 𝑃 ) )
87 84 85 86 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑃 × 𝑃 ) )
88 opelxpi ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑃 × 𝑃 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑃 × 𝑃 ) ) → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) )
89 83 87 88 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) )
90 79 89 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → 𝑓 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) )
91 78 90 anim12dan ⊢ ( ( ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) ) → ( 𝑒 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ∧ 𝑓 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) )
92 91 rexlimdva2 ⊢ ( ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → ( 𝑒 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ∧ 𝑓 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) ) )
93 92 rexlimdva ⊢ ( ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → ( 𝑒 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ∧ 𝑓 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) ) )
94 93 rexlimdva ⊢ ( ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) → ( ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → ( 𝑒 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ∧ 𝑓 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) ) )
95 94 rexlimdva ⊢ ( ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → ( 𝑒 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ∧ 𝑓 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) ) )
96 95 rexlimdva ⊢ ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → ( 𝑒 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ∧ 𝑓 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) ) )
97 96 rexlimdva ⊢ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) → ( ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → ( 𝑒 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ∧ 𝑓 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) ) )
98 97 rexlimivv ⊢ ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ) → ( 𝑒 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ∧ 𝑓 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) )
99 68 98 syl ⊢ ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) → ( 𝑒 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ∧ 𝑓 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) )
100 99 ssopab2i ⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) } ⊆ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ∧ 𝑓 ∈ ( ( 𝑃 × 𝑃 ) × ( 𝑃 × 𝑃 ) ) ) }
101 59 100 ssexi ⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) } ∈ V
102 101 a1i ⊢ ( 𝜑 → { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) } ∈ V )
103 6 53 4 102 fvmptd ⊢ ( 𝜑 → ( AFS ‘ 𝐺 ) = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑒 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑓 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ∧ ( ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) ∧ ( 𝑏 − 𝑐 ) = ( 𝑦 − 𝑧 ) ) ∧ ( ( 𝑎 − 𝑑 ) = ( 𝑥 − 𝑤 ) ∧ ( 𝑏 − 𝑑 ) = ( 𝑦 − 𝑤 ) ) ) ) } )