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 30877
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 30876 . . 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 1081 . . . . . . 7 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → 𝑝 = 𝑃)
76eqcomd 2657 . . . . . 6 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → 𝑃 = 𝑝)
87adantr 480 . . . . . . 7 (((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) → 𝑃 = 𝑝)
98adantr 480 . . . . . . . 8 ((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) → 𝑃 = 𝑝)
109adantr 480 . . . . . . . . 9 (((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) → 𝑃 = 𝑝)
1110adantr 480 . . . . . . . . . 10 ((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) → 𝑃 = 𝑝)
1211adantr 480 . . . . . . . . . . 11 (((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) → 𝑃 = 𝑝)
1312adantr 480 . . . . . . . . . . . 12 ((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) → 𝑃 = 𝑝)
147ad7antr 781 . . . . . . . . . . . . 13 (((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) → 𝑃 = 𝑝)
15 simp3 1083 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → 𝑖 = 𝐼)
1615ad8antr 785 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → 𝑖 = 𝐼)
1716eqcomd 2657 . . . . . . . . . . . . . . . . . 18 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → 𝐼 = 𝑖)
1817oveqd 6707 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑎𝐼𝑐) = (𝑎𝑖𝑐))
1918eleq2d 2716 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝑎𝑖𝑐)))
2017oveqd 6707 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑥𝐼𝑧) = (𝑥𝑖𝑧))
2120eleq2d 2716 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑥𝑖𝑧)))
2219, 21anbi12d 747 . . . . . . . . . . . . . . 15 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧))))
23 simp2 1082 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → = )
2423eqcomd 2657 . . . . . . . . . . . . . . . . . . 19 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → = )
2524ad8antr 785 . . . . . . . . . . . . . . . . . 18 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → = )
2625oveqd 6707 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑎 𝑏) = (𝑎𝑏))
2725oveqd 6707 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑥 𝑦) = (𝑥𝑦))
2826, 27eqeq12d 2666 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑎 𝑏) = (𝑥 𝑦) ↔ (𝑎𝑏) = (𝑥𝑦)))
2925oveqd 6707 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑏 𝑐) = (𝑏𝑐))
3025oveqd 6707 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑦 𝑧) = (𝑦𝑧))
3129, 30eqeq12d 2666 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑏 𝑐) = (𝑦 𝑧) ↔ (𝑏𝑐) = (𝑦𝑧)))
3228, 31anbi12d 747 . . . . . . . . . . . . . . 15 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ↔ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧))))
3325oveqd 6707 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑎 𝑑) = (𝑎𝑑))
3425oveqd 6707 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑥 𝑤) = (𝑥𝑤))
3533, 34eqeq12d 2666 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑎 𝑑) = (𝑥 𝑤) ↔ (𝑎𝑑) = (𝑥𝑤)))
3625oveqd 6707 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑏 𝑑) = (𝑏𝑑))
3725oveqd 6707 . . . . . . . . . . . . . . . . 17 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (𝑦 𝑤) = (𝑦𝑤))
3836, 37eqeq12d 2666 . . . . . . . . . . . . . . . 16 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑏 𝑑) = (𝑦 𝑤) ↔ (𝑏𝑑) = (𝑦𝑤)))
3935, 38anbi12d 747 . . . . . . . . . . . . . . 15 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)) ↔ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
4022, 32, 393anbi123d 1439 . . . . . . . . . . . . . 14 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → (((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))) ↔ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤)))))
41403anbi3d 1445 . . . . . . . . . . . . 13 ((((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4214, 41rexeqbidva 3185 . . . . . . . . . . . 12 (((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) → (∃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4313, 42rexeqbidva 3185 . . . . . . . . . . 11 ((((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) → (∃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4412, 43rexeqbidva 3185 . . . . . . . . . 10 (((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) → (∃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4511, 44rexeqbidva 3185 . . . . . . . . 9 ((((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) → (∃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
4610, 45rexeqbidva 3185 . . . . . . . 8 (((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) ∧ 𝑐𝑃) → (∃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
479, 46rexeqbidva 3185 . . . . . . 7 ((((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) ∧ 𝑏𝑃) → (∃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
488, 47rexeqbidva 3185 . . . . . 6 (((𝑝 = 𝑃 = 𝑖 = 𝐼) ∧ 𝑎𝑃) → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
497, 48rexeqbidva 3185 . . . . 5 ((𝑝 = 𝑃 = 𝑖 = 𝐼) → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) ↔ ∃𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))))
503, 4, 5, 49sbcie3s 15964 . . . 4 (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤)))) ↔ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))))
5150adantl 481 . . 3 ((𝜑𝑔 = 𝐺) → ([(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤)))) ↔ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))))
5251opabbidv 4749 . 2 ((𝜑𝑔 = 𝐺) → {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))} = {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))})
53 brafs.g . 2 (𝜑𝐺 ∈ TarskiG)
54 df-xp 5149 . . . . 5 (((𝑃 × 𝑃) × (𝑃 × 𝑃)) × ((𝑃 × 𝑃) × (𝑃 × 𝑃))) = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))}
55 fvex 6239 . . . . . . . . 9 (Base‘𝐺) ∈ V
563, 55eqeltri 2726 . . . . . . . 8 𝑃 ∈ V
5756, 56xpex 7004 . . . . . . 7 (𝑃 × 𝑃) ∈ V
5857, 57xpex 7004 . . . . . 6 ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∈ V
5958, 58xpex 7004 . . . . 5 (((𝑃 × 𝑃) × (𝑃 × 𝑃)) × ((𝑃 × 𝑃) × (𝑃 × 𝑃))) ∈ V
6054, 59eqeltrri 2727 . . . 4 {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))} ∈ V
61 3simpa 1078 . . . . . . . . . . . . . 14 ((𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6261reximi 3040 . . . . . . . . . . . . 13 (∃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6362reximi 3040 . . . . . . . . . . . 12 (∃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6463reximi 3040 . . . . . . . . . . 11 (∃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6564reximi 3040 . . . . . . . . . 10 (∃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6665reximi 3040 . . . . . . . . 9 (∃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6766reximi 3040 . . . . . . . 8 (∃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6867reximi 3040 . . . . . . 7 (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
6968reximi 3040 . . . . . 6 (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩))
70 simpr 476 . . . . . . . . . . . . . . . 16 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩)
71 opelxpi 5182 . . . . . . . . . . . . . . . . . 18 ((𝑎𝑃𝑏𝑃) → ⟨𝑎, 𝑏⟩ ∈ (𝑃 × 𝑃))
7271ad7antr 781 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → ⟨𝑎, 𝑏⟩ ∈ (𝑃 × 𝑃))
73 simp-7r 830 . . . . . . . . . . . . . . . . . 18 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → 𝑐𝑃)
74 simp-6r 828 . . . . . . . . . . . . . . . . . 18 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → 𝑑𝑃)
75 opelxpi 5182 . . . . . . . . . . . . . . . . . 18 ((𝑐𝑃𝑑𝑃) → ⟨𝑐, 𝑑⟩ ∈ (𝑃 × 𝑃))
7673, 74, 75syl2anc 694 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → ⟨𝑐, 𝑑⟩ ∈ (𝑃 × 𝑃))
77 opelxpi 5182 . . . . . . . . . . . . . . . . 17 ((⟨𝑎, 𝑏⟩ ∈ (𝑃 × 𝑃) ∧ ⟨𝑐, 𝑑⟩ ∈ (𝑃 × 𝑃)) → ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
7872, 76, 77syl2anc 694 . . . . . . . . . . . . . . . 16 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
7970, 78eqeltrd 2730 . . . . . . . . . . . . . . 15 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) → 𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
80 simpr 476 . . . . . . . . . . . . . . . 16 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩)
81 simp-5r 826 . . . . . . . . . . . . . . . . . 18 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑥𝑃)
82 simp-4r 824 . . . . . . . . . . . . . . . . . 18 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑦𝑃)
83 opelxpi 5182 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑃𝑦𝑃) → ⟨𝑥, 𝑦⟩ ∈ (𝑃 × 𝑃))
8481, 82, 83syl2anc 694 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → ⟨𝑥, 𝑦⟩ ∈ (𝑃 × 𝑃))
85 simpllr 815 . . . . . . . . . . . . . . . . . 18 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑧𝑃)
86 simplr 807 . . . . . . . . . . . . . . . . . 18 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑤𝑃)
87 opelxpi 5182 . . . . . . . . . . . . . . . . . 18 ((𝑧𝑃𝑤𝑃) → ⟨𝑧, 𝑤⟩ ∈ (𝑃 × 𝑃))
8885, 86, 87syl2anc 694 . . . . . . . . . . . . . . . . 17 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → ⟨𝑧, 𝑤⟩ ∈ (𝑃 × 𝑃))
89 opelxpi 5182 . . . . . . . . . . . . . . . . 17 ((⟨𝑥, 𝑦⟩ ∈ (𝑃 × 𝑃) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑃 × 𝑃)) → ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
9084, 88, 89syl2anc 694 . . . . . . . . . . . . . . . 16 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
9180, 90eqeltrd 2730 . . . . . . . . . . . . . . 15 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))
9279, 91anim12dan 900 . . . . . . . . . . . . . 14 (((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) ∧ (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩)) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃))))
9392ex 449 . . . . . . . . . . . . 13 ((((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑤𝑃) → ((𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9493rexlimdva 3060 . . . . . . . . . . . 12 (((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) → (∃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9594rexlimdva 3060 . . . . . . . . . . 11 ((((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) ∧ 𝑦𝑃) → (∃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9695rexlimdva 3060 . . . . . . . . . 10 (((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑥𝑃) → (∃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9796rexlimdva 3060 . . . . . . . . 9 ((((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) → (∃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9897rexlimdva 3060 . . . . . . . 8 (((𝑎𝑃𝑏𝑃) ∧ 𝑐𝑃) → (∃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
9998rexlimdva 3060 . . . . . . 7 ((𝑎𝑃𝑏𝑃) → (∃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))))
10099rexlimivv 3065 . . . . . 6 (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃))))
10169, 100syl 17 . . . . 5 (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤)))) → (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃))))
102101ssopab2i 5032 . . . 4 {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))} ⊆ {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)) ∧ 𝑓 ∈ ((𝑃 × 𝑃) × (𝑃 × 𝑃)))}
10360, 102ssexi 4836 . . 3 {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))} ∈ V
104103a1i 11 . 2 (𝜑 → {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))} ∈ V)
1052, 52, 53, 104fvmptd 6327 1 (𝜑 → (AFS‘𝐺) = {⟨𝑒, 𝑓⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑥𝑃𝑦𝑃𝑧𝑃𝑤𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 𝑏) = (𝑥 𝑦) ∧ (𝑏 𝑐) = (𝑦 𝑧)) ∧ ((𝑎 𝑑) = (𝑥 𝑤) ∧ (𝑏 𝑑) = (𝑦 𝑤))))})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wrex 2942  Vcvv 3231  [wsbc 3468  cop 4216  {copab 4745  cmpt 4762   × cxp 5141  cfv 5926  (class class class)co 6690  Basecbs 15904  distcds 15997  TarskiGcstrkg 25374  Itvcitv 25380  AFScafs 30875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-iota 5889  df-fun 5928  df-fv 5934  df-ov 6693  df-afs 30876
This theorem is referenced by:  brafs  30878
  Copyright terms: Public domain W3C validator