Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  reuop Structured version   Visualization version   GIF version

Theorem reuop 6128
 Description: There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 23-Jun-2023.)
Hypotheses
Ref Expression
reu3op.a (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜓𝜒))
reuop.x (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜓𝜃))
Assertion
Ref Expression
reuop (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑎𝑋𝑏𝑌 (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
Distinct variable groups:   𝑋,𝑎,𝑏,𝑝,𝑥,𝑦   𝑌,𝑎,𝑏,𝑝,𝑥,𝑦   𝜓,𝑎,𝑏,𝑥,𝑦   𝜒,𝑝   𝜃,𝑝
Allowed substitution hints:   𝜓(𝑝)   𝜒(𝑥,𝑦,𝑎,𝑏)   𝜃(𝑥,𝑦,𝑎,𝑏)

Proof of Theorem reuop
Dummy variables 𝑞 𝑐 𝑑 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfsbc1v 3719 . . 3 𝑝[𝑞 / 𝑝]𝜓
2 nfsbc1v 3719 . . 3 𝑝[𝑤 / 𝑝]𝜓
3 sbceq1a 3710 . . 3 (𝑝 = 𝑤 → (𝜓[𝑤 / 𝑝]𝜓))
4 dfsbcq 3701 . . 3 (𝑤 = 𝑞 → ([𝑤 / 𝑝]𝜓[𝑞 / 𝑝]𝜓))
51, 2, 3, 4reu8nf 3786 . 2 (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)))
6 elxp2 5553 . . . . 5 (𝑝 ∈ (𝑋 × 𝑌) ↔ ∃𝑎𝑋𝑏𝑌 𝑝 = ⟨𝑎, 𝑏⟩)
7 reu3op.a . . . . . . . . . . . . 13 (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜓𝜒))
87biimpcd 252 . . . . . . . . . . . 12 (𝜓 → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
98adantr 484 . . . . . . . . . . 11 ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
109adantr 484 . . . . . . . . . 10 (((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) ∧ (𝑎𝑋𝑏𝑌)) → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
1110imp 410 . . . . . . . . 9 ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) ∧ (𝑎𝑋𝑏𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → 𝜒)
12 opelxpi 5566 . . . . . . . . . . . . . . . 16 ((𝑥𝑋𝑦𝑌) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌))
13 dfsbcq 3701 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑥, 𝑦⟩ → ([𝑞 / 𝑝]𝜓[𝑥, 𝑦⟩ / 𝑝]𝜓))
14 eqeq2 2771 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑥, 𝑦⟩ → (𝑝 = 𝑞𝑝 = ⟨𝑥, 𝑦⟩))
1513, 14imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑞 = ⟨𝑥, 𝑦⟩ → (([𝑞 / 𝑝]𝜓𝑝 = 𝑞) ↔ ([𝑥, 𝑦⟩ / 𝑝]𝜓𝑝 = ⟨𝑥, 𝑦⟩)))
1615adantl 485 . . . . . . . . . . . . . . . 16 (((𝑥𝑋𝑦𝑌) ∧ 𝑞 = ⟨𝑥, 𝑦⟩) → (([𝑞 / 𝑝]𝜓𝑝 = 𝑞) ↔ ([𝑥, 𝑦⟩ / 𝑝]𝜓𝑝 = ⟨𝑥, 𝑦⟩)))
1712, 16rspcdv 3536 . . . . . . . . . . . . . . 15 ((𝑥𝑋𝑦𝑌) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞) → ([𝑥, 𝑦⟩ / 𝑝]𝜓𝑝 = ⟨𝑥, 𝑦⟩)))
1817adantr 484 . . . . . . . . . . . . . 14 (((𝑥𝑋𝑦𝑌) ∧ 𝜓) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞) → ([𝑥, 𝑦⟩ / 𝑝]𝜓𝑝 = ⟨𝑥, 𝑦⟩)))
19 opex 5329 . . . . . . . . . . . . . . . . . . . 20 𝑥, 𝑦⟩ ∈ V
20 reuop.x . . . . . . . . . . . . . . . . . . . 20 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜓𝜃))
2119, 20sbcie 3740 . . . . . . . . . . . . . . . . . . 19 ([𝑥, 𝑦⟩ / 𝑝]𝜓𝜃)
22 pm2.27 42 . . . . . . . . . . . . . . . . . . 19 ([𝑥, 𝑦⟩ / 𝑝]𝜓 → (([𝑥, 𝑦⟩ / 𝑝]𝜓𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩))
2321, 22sylbir 238 . . . . . . . . . . . . . . . . . 18 (𝜃 → (([𝑥, 𝑦⟩ / 𝑝]𝜓𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩))
24 eqcom 2766 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ = 𝑝𝑝 = ⟨𝑥, 𝑦⟩)
2523, 24syl6ibr 255 . . . . . . . . . . . . . . . . 17 (𝜃 → (([𝑥, 𝑦⟩ / 𝑝]𝜓𝑝 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ = 𝑝))
2625com12 32 . . . . . . . . . . . . . . . 16 (([𝑥, 𝑦⟩ / 𝑝]𝜓𝑝 = ⟨𝑥, 𝑦⟩) → (𝜃 → ⟨𝑥, 𝑦⟩ = 𝑝))
27 eqeq2 2771 . . . . . . . . . . . . . . . . . 18 (⟨𝑎, 𝑏⟩ = 𝑝 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = 𝑝))
2827eqcoms 2767 . . . . . . . . . . . . . . . . 17 (𝑝 = ⟨𝑎, 𝑏⟩ → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = 𝑝))
2928imbi2d 344 . . . . . . . . . . . . . . . 16 (𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ (𝜃 → ⟨𝑥, 𝑦⟩ = 𝑝)))
3026, 29syl5ibrcom 250 . . . . . . . . . . . . . . 15 (([𝑥, 𝑦⟩ / 𝑝]𝜓𝑝 = ⟨𝑥, 𝑦⟩) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
3130a1d 25 . . . . . . . . . . . . . 14 (([𝑥, 𝑦⟩ / 𝑝]𝜓𝑝 = ⟨𝑥, 𝑦⟩) → ((𝑎𝑋𝑏𝑌) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
3218, 31syl6 35 . . . . . . . . . . . . 13 (((𝑥𝑋𝑦𝑌) ∧ 𝜓) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞) → ((𝑎𝑋𝑏𝑌) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))))
3332expimpd 457 . . . . . . . . . . . 12 ((𝑥𝑋𝑦𝑌) → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) → ((𝑎𝑋𝑏𝑌) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))))
3433imp4c 427 . . . . . . . . . . 11 ((𝑥𝑋𝑦𝑌) → ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) ∧ (𝑎𝑋𝑏𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
3534impcom 411 . . . . . . . . . 10 (((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) ∧ (𝑎𝑋𝑏𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) ∧ (𝑥𝑋𝑦𝑌)) → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
3635ralrimivva 3121 . . . . . . . . 9 ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) ∧ (𝑎𝑋𝑏𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
3711, 36jca 515 . . . . . . . 8 ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) ∧ (𝑎𝑋𝑏𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
3837ex 416 . . . . . . 7 (((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) ∧ (𝑎𝑋𝑏𝑌)) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
3938reximdvva 3202 . . . . . 6 ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) → (∃𝑎𝑋𝑏𝑌 𝑝 = ⟨𝑎, 𝑏⟩ → ∃𝑎𝑋𝑏𝑌 (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
4039com12 32 . . . . 5 (∃𝑎𝑋𝑏𝑌 𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) → ∃𝑎𝑋𝑏𝑌 (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
416, 40sylbi 220 . . . 4 (𝑝 ∈ (𝑋 × 𝑌) → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) → ∃𝑎𝑋𝑏𝑌 (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
4241rexlimiv 3205 . . 3 (∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) → ∃𝑎𝑋𝑏𝑌 (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
43 opelxpi 5566 . . . . . . 7 ((𝑎𝑋𝑏𝑌) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
4443adantr 484 . . . . . 6 (((𝑎𝑋𝑏𝑌) ∧ (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
45 simprl 770 . . . . . 6 (((𝑎𝑋𝑏𝑌) ∧ (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → 𝜒)
46 nfsbc1v 3719 . . . . . . . . . . . . . . . . . 18 𝑥[𝑐 / 𝑥]𝜃
47 nfv 1916 . . . . . . . . . . . . . . . . . 18 𝑥𝑐, 𝑦⟩ = ⟨𝑎, 𝑏
4846, 47nfim 1898 . . . . . . . . . . . . . . . . 17 𝑥([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩)
49 nfsbc1v 3719 . . . . . . . . . . . . . . . . . 18 𝑦[𝑑 / 𝑦][𝑐 / 𝑥]𝜃
50 nfv 1916 . . . . . . . . . . . . . . . . . 18 𝑦𝑐, 𝑑⟩ = ⟨𝑎, 𝑏
5149, 50nfim 1898 . . . . . . . . . . . . . . . . 17 𝑦([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
52 sbceq1a 3710 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑐 → (𝜃[𝑐 / 𝑥]𝜃))
53 opeq1 4765 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑐 → ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑦⟩)
5453eqeq1d 2761 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑐 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
5552, 54imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑐 → ((𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ ([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
56 sbceq1a 3710 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑑 → ([𝑐 / 𝑥]𝜃[𝑑 / 𝑦][𝑐 / 𝑥]𝜃))
57 opeq2 4767 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑑 → ⟨𝑐, 𝑦⟩ = ⟨𝑐, 𝑑⟩)
5857eqeq1d 2761 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑑 → (⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
5956, 58imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑑 → (([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
6048, 51, 55, 59rspc2 3552 . . . . . . . . . . . . . . . 16 ((𝑐𝑋𝑑𝑌) → (∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
6160ad2antlr 726 . . . . . . . . . . . . . . 15 ((((𝑎𝑋𝑏𝑌) ∧ (𝑐𝑋𝑑𝑌)) ∧ 𝜒) → (∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
6220sbcop 5353 . . . . . . . . . . . . . . . . . 18 ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃[𝑐, 𝑑⟩ / 𝑝]𝜓)
63 pm2.27 42 . . . . . . . . . . . . . . . . . 18 ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
6462, 63sylbir 238 . . . . . . . . . . . . . . . . 17 ([𝑐, 𝑑⟩ / 𝑝]𝜓 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
65 eqcom 2766 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
6664, 65syl6ibr 255 . . . . . . . . . . . . . . . 16 ([𝑐, 𝑑⟩ / 𝑝]𝜓 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
6766com12 32 . . . . . . . . . . . . . . 15 (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ([𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
6861, 67syl6 35 . . . . . . . . . . . . . 14 ((((𝑎𝑋𝑏𝑌) ∧ (𝑐𝑋𝑑𝑌)) ∧ 𝜒) → (∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
6968expimpd 457 . . . . . . . . . . . . 13 (((𝑎𝑋𝑏𝑌) ∧ (𝑐𝑋𝑑𝑌)) → ((𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ([𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
7069expcom 417 . . . . . . . . . . . 12 ((𝑐𝑋𝑑𝑌) → ((𝑎𝑋𝑏𝑌) → ((𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ([𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))))
7170impd 414 . . . . . . . . . . 11 ((𝑐𝑋𝑑𝑌) → (((𝑎𝑋𝑏𝑌) ∧ (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ([𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
7271impcom 411 . . . . . . . . . 10 ((((𝑎𝑋𝑏𝑌) ∧ (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ (𝑐𝑋𝑑𝑌)) → ([𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
73 dfsbcq 3701 . . . . . . . . . . 11 (𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓[𝑐, 𝑑⟩ / 𝑝]𝜓))
74 eqeq2 2771 . . . . . . . . . . 11 (𝑞 = ⟨𝑐, 𝑑⟩ → (⟨𝑎, 𝑏⟩ = 𝑞 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
7573, 74imbi12d 348 . . . . . . . . . 10 (𝑞 = ⟨𝑐, 𝑑⟩ → (([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞) ↔ ([𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
7672, 75syl5ibrcom 250 . . . . . . . . 9 ((((𝑎𝑋𝑏𝑌) ∧ (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ (𝑐𝑋𝑑𝑌)) → (𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
7776rexlimdvva 3219 . . . . . . . 8 (((𝑎𝑋𝑏𝑌) ∧ (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → (∃𝑐𝑋𝑑𝑌 𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
78 elxp2 5553 . . . . . . . . 9 (𝑞 ∈ (𝑋 × 𝑌) ↔ ∃𝑐𝑋𝑑𝑌 𝑞 = ⟨𝑐, 𝑑⟩)
7978biimpi 219 . . . . . . . 8 (𝑞 ∈ (𝑋 × 𝑌) → ∃𝑐𝑋𝑑𝑌 𝑞 = ⟨𝑐, 𝑑⟩)
8077, 79impel 509 . . . . . . 7 ((((𝑎𝑋𝑏𝑌) ∧ (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ 𝑞 ∈ (𝑋 × 𝑌)) → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
8180ralrimiva 3114 . . . . . 6 (((𝑎𝑋𝑏𝑌) ∧ (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
82 nfv 1916 . . . . . . . 8 𝑝𝜒
83 nfcv 2920 . . . . . . . . 9 𝑝(𝑋 × 𝑌)
84 nfv 1916 . . . . . . . . . 10 𝑝𝑎, 𝑏⟩ = 𝑞
851, 84nfim 1898 . . . . . . . . 9 𝑝([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)
8683, 85nfralw 3154 . . . . . . . 8 𝑝𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)
8782, 86nfan 1901 . . . . . . 7 𝑝(𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
88 eqeq1 2763 . . . . . . . . . 10 (𝑝 = ⟨𝑎, 𝑏⟩ → (𝑝 = 𝑞 ↔ ⟨𝑎, 𝑏⟩ = 𝑞))
8988imbi2d 344 . . . . . . . . 9 (𝑝 = ⟨𝑎, 𝑏⟩ → (([𝑞 / 𝑝]𝜓𝑝 = 𝑞) ↔ ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
9089ralbidv 3127 . . . . . . . 8 (𝑝 = ⟨𝑎, 𝑏⟩ → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞) ↔ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
917, 90anbi12d 633 . . . . . . 7 (𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) ↔ (𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))))
9287, 91rspce 3533 . . . . . 6 ((⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌) ∧ (𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)))
9344, 45, 81, 92syl12anc 835 . . . . 5 (((𝑎𝑋𝑏𝑌) ∧ (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)))
9493ex 416 . . . 4 ((𝑎𝑋𝑏𝑌) → ((𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞))))
9594rexlimivv 3217 . . 3 (∃𝑎𝑋𝑏𝑌 (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)))
9642, 95impbii 212 . 2 (∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓𝑝 = 𝑞)) ↔ ∃𝑎𝑋𝑏𝑌 (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
975, 96bitri 278 1 (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑎𝑋𝑏𝑌 (𝜒 ∧ ∀𝑥𝑋𝑦𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1539   ∈ wcel 2112  ∀wral 3071  ∃wrex 3072  ∃!wreu 3073  [wsbc 3699  ⟨cop 4532   × cxp 5527 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5174  ax-nul 5181  ax-pr 5303 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-nul 4229  df-if 4425  df-sn 4527  df-pr 4529  df-op 4533  df-opab 5100  df-xp 5535 This theorem is referenced by:  ichnreuop  44417  ichreuopeq  44418  reuopreuprim  44471
 Copyright terms: Public domain W3C validator