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

Theorem afsval 32174
 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 32173 . . 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 1133 . . . . . . 7 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → 𝑝 = 𝑃)
76eqcomd 2764 . . . . . 6 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → 𝑃 = 𝑝)
87adantr 484 . . . . . . 7 (((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) → 𝑃 = 𝑝)
98adantr 484 . . . . . . . 8 ((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) → 𝑃 = 𝑝)
109adantr 484 . . . . . . . . 9 (((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) → 𝑃 = 𝑝)
1110adantr 484 . . . . . . . . . 10 ((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) → 𝑃 = 𝑝)
1211adantr 484 . . . . . . . . . . 11 (((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) → 𝑃 = 𝑝)
1312adantr 484 . . . . . . . . . . . 12 ((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) → 𝑃 = 𝑝)
147ad7antr 737 . . . . . . . . . . . . 13 (((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) → 𝑃 = 𝑝)
15 simp3 1135 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → 𝑖 = 𝐼)
1615ad8antr 739 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → 𝑖 = 𝐼)
1716eqcomd 2764 . . . . . . . . . . . . . . . . . 18 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → 𝐼 = 𝑖)
1817oveqd 7172 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑎𝐼𝑐) = (𝑎𝑖𝑐))
1918eleq2d 2837 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝑎𝑖𝑐)))
2017oveqd 7172 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑥𝐼𝑧) = (𝑥𝑖𝑧))
2120eleq2d 2837 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑥𝑖𝑧)))
2219, 21anbi12d 633 . . . . . . . . . . . . . . 15 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧))))
23 simp2 1134 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → = )
2423eqcomd 2764 . . . . . . . . . . . . . . . . . . 19 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → = )
2524ad8antr 739 . . . . . . . . . . . . . . . . . 18 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → = )
2625oveqd 7172 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑎 𝑏) = (𝑎𝑏))
2725oveqd 7172 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑥 𝑦) = (𝑥𝑦))
2826, 27eqeq12d 2774 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑎 𝑏) = (𝑥 𝑦) ↔ (𝑎𝑏) = (𝑥𝑦)))
2925oveqd 7172 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑏 𝑐) = (𝑏𝑐))
3025oveqd 7172 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑦 𝑧) = (𝑦𝑧))
3129, 30eqeq12d 2774 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑏 𝑐) = (𝑦 𝑧) ↔ (𝑏𝑐) = (𝑦𝑧)))
3228, 31anbi12d 633 . . . . . . . . . . . . . . 15 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ↔ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧))))
3325oveqd 7172 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑎 𝑑) = (𝑎𝑑))
3425oveqd 7172 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑥 𝑤) = (𝑥𝑤))
3533, 34eqeq12d 2774 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑎 𝑑) = (𝑥 𝑤) ↔ (𝑎𝑑) = (𝑥𝑤)))
3625oveqd 7172 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑏 𝑑) = (𝑏𝑑))
3725oveqd 7172 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑦 𝑤) = (𝑦𝑤))
3836, 37eqeq12d 2774 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑏 𝑑) = (𝑦 𝑤) ↔ (𝑏𝑑) = (𝑦𝑤)))
3935, 38anbi12d 633 . . . . . . . . . . . . . . 15 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)) ↔ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
4022, 32, 393anbi123d 1433 . . . . . . . . . . . . . 14 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))) ↔ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤)))))
41403anbi3d 1439 . . . . . . . . . . . . 13 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4214, 41rexeqbidva 3336 . . . . . . . . . . . 12 (((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) → (∃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4313, 42rexeqbidva 3336 . . . . . . . . . . 11 ((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) → (∃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4412, 43rexeqbidva 3336 . . . . . . . . . 10 (((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) → (∃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4511, 44rexeqbidva 3336 . . . . . . . . 9 ((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) → (∃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4610, 45rexeqbidva 3336 . . . . . . . 8 (((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) → (∃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
479, 46rexeqbidva 3336 . . . . . . 7 ((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) → (∃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
488, 47rexeqbidva 3336 . . . . . 6 (((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
497, 48rexeqbidva 3336 . . . . 5 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
503, 4, 5, 49sbcie3s 16604 . . . 4 (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤)))) ↔ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))))
5150adantl 485 . . 3 ((𝜑𝑔 = 𝐺) → ([(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤)))) ↔ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))))
5251opabbidv 5101 . 2 ((𝜑𝑔 = 𝐺) → {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))} = {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))})
53 brafs.g . 2 (𝜑𝐺 ∈ TarskiG)
54 df-xp 5533 . . . . 5 (((𝑃 × 𝑃) × (𝑃 × 𝑃)) × ((𝑃 × 𝑃) × (𝑃 × 𝑃))) = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))}
553fvexi 6676 . . . . . . . 8 𝑃 ∈ V
5655, 55xpex 7479 . . . . . . 7 (𝑃 × 𝑃) ∈ V
5756, 56xpex 7479 . . . . . 6 ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∈ V
5857, 57xpex 7479 . . . . 5 (((𝑃 × 𝑃) × (𝑃 × 𝑃)) × ((𝑃 × 𝑃) × (𝑃 × 𝑃))) ∈ V
5954, 58eqeltrri 2849 . . . 4 {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))} ∈ V
60 3simpa 1145 . . . . . . . . . . . . . 14 ((𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6160reximi 3171 . . . . . . . . . . . . 13 (∃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6261reximi 3171 . . . . . . . . . . . 12 (∃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6362reximi 3171 . . . . . . . . . . 11 (∃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6463reximi 3171 . . . . . . . . . 10 (∃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6564reximi 3171 . . . . . . . . 9 (∃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6665reximi 3171 . . . . . . . 8 (∃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6766reximi 3171 . . . . . . 7 (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6867reximi 3171 . . . . . 6 (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
69 simpr 488 . . . . . . . . . . . . . . 15 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩)
70 opelxpi 5564 . . . . . . . . . . . . . . . . 17 ((𝑎𝑃𝑏𝑃) → ⟨𝑎, 𝑏⟩ ∈ (𝑃 × 𝑃))
7170ad7antr 737 . . . . . . . . . . . . . . . 16 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → ⟨𝑎, 𝑏⟩ ∈ (𝑃 × 𝑃))
72 simp-7r 789 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → 𝑐𝑃)
73 simp-6r 787 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → 𝑑𝑃)
74 opelxpi 5564 . . . . . . . . . . . . . . . . 17 ((𝑐𝑃𝑑𝑃) → ⟨𝑐, 𝑑⟩ ∈ (𝑃 × 𝑃))
7572, 73, 74syl2anc 587 . . . . . . . . . . . . . . . 16 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → ⟨𝑐, 𝑑⟩ ∈ (𝑃 × 𝑃))
76 opelxpi 5564 . . . . . . . . . . . . . . . 16 ((⟨𝑎, 𝑏⟩ ∈ (𝑃 × 𝑃) ∧ ⟨𝑐, 𝑑⟩ ∈ (𝑃 × 𝑃)) → ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
7771, 75, 76syl2anc 587 . . . . . . . . . . . . . . 15 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
7869, 77eqeltrd 2852 . . . . . . . . . . . . . 14 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → 𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
79 simpr 488 . . . . . . . . . . . . . . 15 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩)
80 simp-5r 785 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑥𝑃)
81 simp-4r 783 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑦𝑃)
82 opelxpi 5564 . . . . . . . . . . . . . . . . 17 ((𝑥𝑃𝑦𝑃) → ⟨𝑥, 𝑦⟩ ∈ (𝑃 × 𝑃))
8380, 81, 82syl2anc 587 . . . . . . . . . . . . . . . 16 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → ⟨𝑥, 𝑦⟩ ∈ (𝑃 × 𝑃))
84 simpllr 775 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑧𝑃)
85 simplr 768 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑤𝑃)
86 opelxpi 5564 . . . . . . . . . . . . . . . . 17 ((𝑧𝑃𝑤𝑃) → ⟨𝑧, 𝑤⟩ ∈ (𝑃 × 𝑃))
8784, 85, 86syl2anc 587 . . . . . . . . . . . . . . . 16 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → ⟨𝑧, 𝑤⟩ ∈ (𝑃 × 𝑃))
88 opelxpi 5564 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ ∈ (𝑃 × 𝑃) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑃 × 𝑃)) → ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
8983, 87, 88syl2anc 587 . . . . . . . . . . . . . . 15 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
9079, 89eqeltrd 2852 . . . . . . . . . . . . . 14 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
9178, 90anim12dan 621 . . . . . . . . . . . . 13 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩)) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃))))
9291rexlimdva2 3211 . . . . . . . . . . . 12 (((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) → (∃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9392rexlimdva 3208 . . . . . . . . . . 11 ((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) → (∃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9493rexlimdva 3208 . . . . . . . . . 10 (((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) → (∃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9594rexlimdva 3208 . . . . . . . . 9 ((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) → (∃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9695rexlimdva 3208 . . . . . . . 8 (((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) → (∃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9796rexlimdva 3208 . . . . . . 7 ((𝑎𝑃𝑏𝑃) → (∃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9897rexlimivv 3216 . . . . . 6 (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃))))
9968, 98syl 17 . . . . 5 (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃))))
10099ssopab2i 5410 . . . 4 {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))} ⊆ {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))}
10159, 100ssexi 5195 . . 3 {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))} ∈ V
102101a1i 11 . 2 (𝜑 → {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))} ∈ V)
1032, 52, 53, 102fvmptd 6770 1 (𝜑 → (AFS‘𝐺) = {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∃wrex 3071  Vcvv 3409  [wsbc 3698  ⟨cop 4531  {copab 5097   ↦ cmpt 5115   × cxp 5525  ‘cfv 6339  (class class class)co 7155  Basecbs 16546  distcds 16637  TarskiGcstrkg 26328  Itvcitv 26334  AFScafs 32172 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-mpt 5116  df-id 5433  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-iota 6298  df-fun 6341  df-fv 6347  df-ov 7158  df-afs 32173 This theorem is referenced by:  brafs  32175
 Copyright terms: Public domain W3C validator