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 30456
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 30455 . . 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 1059 . . . . . . 7 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → 𝑝 = 𝑃)
76eqcomd 2627 . . . . . 6 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → 𝑃 = 𝑝)
87adantr 481 . . . . . . 7 (((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) → 𝑃 = 𝑝)
98adantr 481 . . . . . . . 8 ((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) → 𝑃 = 𝑝)
109adantr 481 . . . . . . . . 9 (((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) → 𝑃 = 𝑝)
1110adantr 481 . . . . . . . . . 10 ((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) → 𝑃 = 𝑝)
1211adantr 481 . . . . . . . . . . 11 (((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) → 𝑃 = 𝑝)
1312adantr 481 . . . . . . . . . . . 12 ((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) → 𝑃 = 𝑝)
147ad7antr 773 . . . . . . . . . . . . 13 (((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) → 𝑃 = 𝑝)
15 simp3 1061 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → 𝑖 = 𝐼)
1615ad8antr 775 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → 𝑖 = 𝐼)
1716eqcomd 2627 . . . . . . . . . . . . . . . . . 18 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → 𝐼 = 𝑖)
1817oveqd 6621 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑎𝐼𝑐) = (𝑎𝑖𝑐))
1918eleq2d 2684 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝑎𝑖𝑐)))
2017oveqd 6621 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑥𝐼𝑧) = (𝑥𝑖𝑧))
2120eleq2d 2684 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑥𝑖𝑧)))
2219, 21anbi12d 746 . . . . . . . . . . . . . . 15 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧))))
23 simp2 1060 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → = )
2423eqcomd 2627 . . . . . . . . . . . . . . . . . . 19 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → = )
2524ad8antr 775 . . . . . . . . . . . . . . . . . 18 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → = )
2625oveqd 6621 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑎 𝑏) = (𝑎𝑏))
2725oveqd 6621 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑥 𝑦) = (𝑥𝑦))
2826, 27eqeq12d 2636 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑎 𝑏) = (𝑥 𝑦) ↔ (𝑎𝑏) = (𝑥𝑦)))
2925oveqd 6621 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑏 𝑐) = (𝑏𝑐))
3025oveqd 6621 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑦 𝑧) = (𝑦𝑧))
3129, 30eqeq12d 2636 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑏 𝑐) = (𝑦 𝑧) ↔ (𝑏𝑐) = (𝑦𝑧)))
3228, 31anbi12d 746 . . . . . . . . . . . . . . 15 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ↔ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧))))
3325oveqd 6621 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑎 𝑑) = (𝑎𝑑))
3425oveqd 6621 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑥 𝑤) = (𝑥𝑤))
3533, 34eqeq12d 2636 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑎 𝑑) = (𝑥 𝑤) ↔ (𝑎𝑑) = (𝑥𝑤)))
3625oveqd 6621 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑏 𝑑) = (𝑏𝑑))
3725oveqd 6621 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑦 𝑤) = (𝑦𝑤))
3836, 37eqeq12d 2636 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑏 𝑑) = (𝑦 𝑤) ↔ (𝑏𝑑) = (𝑦𝑤)))
3935, 38anbi12d 746 . . . . . . . . . . . . . . 15 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)) ↔ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
4022, 32, 393anbi123d 1396 . . . . . . . . . . . . . 14 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))) ↔ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤)))))
41403anbi3d 1402 . . . . . . . . . . . . 13 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4214, 41rexeqbidva 3144 . . . . . . . . . . . 12 (((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) → (∃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4313, 42rexeqbidva 3144 . . . . . . . . . . 11 ((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) → (∃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4412, 43rexeqbidva 3144 . . . . . . . . . 10 (((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) → (∃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4511, 44rexeqbidva 3144 . . . . . . . . 9 ((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) → (∃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4610, 45rexeqbidva 3144 . . . . . . . 8 (((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) → (∃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
479, 46rexeqbidva 3144 . . . . . . 7 ((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) → (∃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
488, 47rexeqbidva 3144 . . . . . 6 (((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
497, 48rexeqbidva 3144 . . . . 5 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
503, 4, 5, 49sbcie3s 15838 . . . 4 (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤)))) ↔ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))))
5150adantl 482 . . 3 ((𝜑𝑔 = 𝐺) → ([(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤)))) ↔ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))))
5251opabbidv 4678 . 2 ((𝜑𝑔 = 𝐺) → {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))} = {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))})
53 brafs.g . 2 (𝜑𝐺 ∈ TarskiG)
54 df-xp 5080 . . . . 5 (((𝑃 × 𝑃) × (𝑃 × 𝑃)) × ((𝑃 × 𝑃) × (𝑃 × 𝑃))) = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))}
55 fvex 6158 . . . . . . . . 9 (Base‘𝐺) ∈ V
563, 55eqeltri 2694 . . . . . . . 8 𝑃 ∈ V
5756, 56xpex 6915 . . . . . . 7 (𝑃 × 𝑃) ∈ V
5857, 57xpex 6915 . . . . . 6 ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∈ V
5958, 58xpex 6915 . . . . 5 (((𝑃 × 𝑃) × (𝑃 × 𝑃)) × ((𝑃 × 𝑃) × (𝑃 × 𝑃))) ∈ V
6054, 59eqeltrri 2695 . . . 4 {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))} ∈ V
61 3simpa 1056 . . . . . . . . . . . . . 14 ((𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6261reximi 3005 . . . . . . . . . . . . 13 (∃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6362reximi 3005 . . . . . . . . . . . 12 (∃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6463reximi 3005 . . . . . . . . . . 11 (∃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6564reximi 3005 . . . . . . . . . 10 (∃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6665reximi 3005 . . . . . . . . 9 (∃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6766reximi 3005 . . . . . . . 8 (∃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6867reximi 3005 . . . . . . 7 (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6968reximi 3005 . . . . . 6 (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
70 simpr 477 . . . . . . . . . . . . . . . 16 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩)
71 opelxpi 5108 . . . . . . . . . . . . . . . . . 18 ((𝑎𝑃𝑏𝑃) → ⟨𝑎, 𝑏⟩ ∈ (𝑃 × 𝑃))
7271ad7antr 773 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → ⟨𝑎, 𝑏⟩ ∈ (𝑃 × 𝑃))
73 simp-7r 812 . . . . . . . . . . . . . . . . . 18 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → 𝑐𝑃)
74 simp-6r 810 . . . . . . . . . . . . . . . . . 18 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → 𝑑𝑃)
75 opelxpi 5108 . . . . . . . . . . . . . . . . . 18 ((𝑐𝑃𝑑𝑃) → ⟨𝑐, 𝑑⟩ ∈ (𝑃 × 𝑃))
7673, 74, 75syl2anc 692 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → ⟨𝑐, 𝑑⟩ ∈ (𝑃 × 𝑃))
77 opelxpi 5108 . . . . . . . . . . . . . . . . 17 ((⟨𝑎, 𝑏⟩ ∈ (𝑃 × 𝑃) ∧ ⟨𝑐, 𝑑⟩ ∈ (𝑃 × 𝑃)) → ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
7872, 76, 77syl2anc 692 . . . . . . . . . . . . . . . 16 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
7970, 78eqeltrd 2698 . . . . . . . . . . . . . . 15 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → 𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
80 simpr 477 . . . . . . . . . . . . . . . 16 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩)
81 simp-5r 808 . . . . . . . . . . . . . . . . . 18 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑥𝑃)
82 simp-4r 806 . . . . . . . . . . . . . . . . . 18 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑦𝑃)
83 opelxpi 5108 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑃𝑦𝑃) → ⟨𝑥, 𝑦⟩ ∈ (𝑃 × 𝑃))
8481, 82, 83syl2anc 692 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → ⟨𝑥, 𝑦⟩ ∈ (𝑃 × 𝑃))
85 simpllr 798 . . . . . . . . . . . . . . . . . 18 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑧𝑃)
86 simplr 791 . . . . . . . . . . . . . . . . . 18 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑤𝑃)
87 opelxpi 5108 . . . . . . . . . . . . . . . . . 18 ((𝑧𝑃𝑤𝑃) → ⟨𝑧, 𝑤⟩ ∈ (𝑃 × 𝑃))
8885, 86, 87syl2anc 692 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → ⟨𝑧, 𝑤⟩ ∈ (𝑃 × 𝑃))
89 opelxpi 5108 . . . . . . . . . . . . . . . . 17 ((⟨𝑥, 𝑦⟩ ∈ (𝑃 × 𝑃) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑃 × 𝑃)) → ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
9084, 88, 89syl2anc 692 . . . . . . . . . . . . . . . 16 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
9180, 90eqeltrd 2698 . . . . . . . . . . . . . . 15 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
9279, 91anim12dan 881 . . . . . . . . . . . . . 14 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩)) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃))))
9392ex 450 . . . . . . . . . . . . 13 ((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9493rexlimdva 3024 . . . . . . . . . . . 12 (((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) → (∃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9594rexlimdva 3024 . . . . . . . . . . 11 ((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) → (∃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9695rexlimdva 3024 . . . . . . . . . 10 (((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) → (∃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9796rexlimdva 3024 . . . . . . . . 9 ((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) → (∃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9897rexlimdva 3024 . . . . . . . 8 (((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) → (∃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9998rexlimdva 3024 . . . . . . 7 ((𝑎𝑃𝑏𝑃) → (∃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
10099rexlimivv 3029 . . . . . 6 (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃))))
10169, 100syl 17 . . . . 5 (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃))))
102101ssopab2i 4963 . . . 4 {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))} ⊆ {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))}
10360, 102ssexi 4763 . . 3 {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))} ∈ V
104103a1i 11 . 2 (𝜑 → {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))} ∈ V)
1052, 52, 53, 104fvmptd 6245 1 (𝜑 → (AFS‘𝐺) = {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wrex 2908  Vcvv 3186  [wsbc 3417  cop 4154  {copab 4672  cmpt 4673   × cxp 5072  cfv 5847  (class class class)co 6604  Basecbs 15781  distcds 15871  TarskiGcstrkg 25229  Itvcitv 25235  AFScafs 30454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-iota 5810  df-fun 5849  df-fv 5855  df-ov 6607  df-afs 30455
This theorem is referenced by:  brafs  30457
  Copyright terms: Public domain W3C validator