Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ichnreuop Structured version   Visualization version   GIF version

Theorem ichnreuop 44157
 Description: If the setvar variables are interchangeable in a wff, there is never a unique ordered pair with different components fulfilling the wff (because if ⟨𝑎, 𝑏⟩ fulfils the wff, then also ⟨𝑏, 𝑎⟩ fulfils the wff). (Contributed by AV, 27-Aug-2023.)
Assertion
Ref Expression
ichnreuop ([𝑎𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑))
Distinct variable groups:   𝑎,𝑏,𝑝   𝜑,𝑝   𝑋,𝑝
Allowed substitution hints:   𝜑(𝑎,𝑏)   𝑋(𝑎,𝑏)

Proof of Theorem ichnreuop
Dummy variables 𝑐 𝑑 𝑣 𝑤 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 notnotb 318 . . . . . . 7 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ¬ ¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑))
2 nfv 1915 . . . . . . . . 9 𝑐(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)
3 nfv 1915 . . . . . . . . 9 𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)
4 nfv 1915 . . . . . . . . . 10 𝑎𝑥, 𝑦⟩ = ⟨𝑐, 𝑑
5 nfv 1915 . . . . . . . . . 10 𝑎 𝑐𝑑
6 nfsbc1v 3742 . . . . . . . . . 10 𝑎[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
74, 5, 6nf3an 1902 . . . . . . . . 9 𝑎(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
8 nfv 1915 . . . . . . . . . 10 𝑏𝑥, 𝑦⟩ = ⟨𝑐, 𝑑
9 nfv 1915 . . . . . . . . . 10 𝑏 𝑐𝑑
10 nfcv 2955 . . . . . . . . . . 11 𝑏𝑐
11 nfsbc1v 3742 . . . . . . . . . . 11 𝑏[𝑑 / 𝑏]𝜑
1210, 11nfsbcw 3744 . . . . . . . . . 10 𝑏[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
138, 9, 12nf3an 1902 . . . . . . . . 9 𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
14 opeq12 4771 . . . . . . . . . . 11 ((𝑎 = 𝑐𝑏 = 𝑑) → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)
1514eqeq2d 2809 . . . . . . . . . 10 ((𝑎 = 𝑐𝑏 = 𝑑) → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩))
16 simpl 486 . . . . . . . . . . 11 ((𝑎 = 𝑐𝑏 = 𝑑) → 𝑎 = 𝑐)
17 simpr 488 . . . . . . . . . . 11 ((𝑎 = 𝑐𝑏 = 𝑑) → 𝑏 = 𝑑)
1816, 17neeq12d 3048 . . . . . . . . . 10 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎𝑏𝑐𝑑))
19 sbceq1a 3733 . . . . . . . . . . 11 (𝑏 = 𝑑 → (𝜑[𝑑 / 𝑏]𝜑))
20 sbceq1a 3733 . . . . . . . . . . 11 (𝑎 = 𝑐 → ([𝑑 / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
2119, 20sylan9bbr 514 . . . . . . . . . 10 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
2215, 18, 213anbi123d 1433 . . . . . . . . 9 ((𝑎 = 𝑐𝑏 = 𝑑) → ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)))
232, 3, 7, 13, 22cbvex2v 2354 . . . . . . . 8 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑐𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
24 vex 3445 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
25 vex 3445 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
2624, 25opth 5337 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑥 = 𝑐𝑦 = 𝑑))
27 eleq1w 2872 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑑 → (𝑦𝑋𝑑𝑋))
2827biimpcd 252 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑋 → (𝑦 = 𝑑𝑑𝑋))
2928adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑋𝑦𝑋) → (𝑦 = 𝑑𝑑𝑋))
3029adantl 485 . . . . . . . . . . . . . . . . 17 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑦 = 𝑑𝑑𝑋))
3130com12 32 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
3231adantl 485 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
3326, 32sylbi 220 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
34333ad2ant1 1130 . . . . . . . . . . . . 13 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
3534impcom 411 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑𝑋)
36 eleq1w 2872 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑐 → (𝑥𝑋𝑐𝑋))
3736biimpcd 252 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑋 → (𝑥 = 𝑐𝑐𝑋))
3837adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑋𝑦𝑋) → (𝑥 = 𝑐𝑐𝑋))
3938adantl 485 . . . . . . . . . . . . . . . . 17 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 = 𝑐𝑐𝑋))
4039com12 32 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑐 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
4140adantr 484 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
4226, 41sylbi 220 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
43423ad2ant1 1130 . . . . . . . . . . . . 13 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
4443impcom 411 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑐𝑋)
45 eqidd 2799 . . . . . . . . . . . . . . . 16 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩)
46 necom 3040 . . . . . . . . . . . . . . . . . . 19 (𝑐𝑑𝑑𝑐)
4746biimpi 219 . . . . . . . . . . . . . . . . . 18 (𝑐𝑑𝑑𝑐)
48473ad2ant2 1131 . . . . . . . . . . . . . . . . 17 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → 𝑑𝑐)
4948adantl 485 . . . . . . . . . . . . . . . 16 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑𝑐)
50 dfich2 44143 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑎𝑏]𝜑 ↔ ∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
51 2sp 2183 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
52 sbsbc 3726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑑 / 𝑏]𝜑[𝑑 / 𝑏]𝜑)
5352sbbii 2081 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
54 sbsbc 3726 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
5553, 54bitri 278 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
56 sbsbc 3726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑐 / 𝑏]𝜑[𝑐 / 𝑏]𝜑)
5756sbbii 2081 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
58 sbsbc 3726 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
5957, 58bitri 278 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
6051, 55, 593bitr3g 316 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6160biimpd 232 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6250, 61sylbi 220 . . . . . . . . . . . . . . . . . . . . 21 ([𝑎𝑏]𝜑 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6362adantr 484 . . . . . . . . . . . . . . . . . . . 20 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6463com12 32 . . . . . . . . . . . . . . . . . . 19 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
65643ad2ant3 1132 . . . . . . . . . . . . . . . . . 18 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6665impcom 411 . . . . . . . . . . . . . . . . 17 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
67 sbccom 3802 . . . . . . . . . . . . . . . . 17 ([𝑐 / 𝑏][𝑑 / 𝑎]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
6866, 67sylibr 237 . . . . . . . . . . . . . . . 16 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
6945, 49, 683jca 1125 . . . . . . . . . . . . . . 15 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
70 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑏𝑑, 𝑐⟩ = ⟨𝑑, 𝑐
71 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑏 𝑑𝑐
72 nfsbc1v 3742 . . . . . . . . . . . . . . . . 17 𝑏[𝑐 / 𝑏][𝑑 / 𝑎]𝜑
7370, 71, 72nf3an 1902 . . . . . . . . . . . . . . . 16 𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
74 opeq2 4769 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑐 → ⟨𝑑, 𝑏⟩ = ⟨𝑑, 𝑐⟩)
7574eqeq2d 2809 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑐 → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩))
76 neeq2 3050 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑐 → (𝑑𝑏𝑑𝑐))
77 sbceq1a 3733 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑐 → ([𝑑 / 𝑎]𝜑[𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
7875, 76, 773anbi123d 1433 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑐 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑)))
7910, 73, 78spcegf 3540 . . . . . . . . . . . . . . 15 (𝑐𝑋 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)))
8044, 69, 79sylc 65 . . . . . . . . . . . . . 14 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑))
81 nfcv 2955 . . . . . . . . . . . . . . 15 𝑎𝑑
82 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑎𝑑, 𝑐⟩ = ⟨𝑑, 𝑏
83 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑎 𝑑𝑏
84 nfsbc1v 3742 . . . . . . . . . . . . . . . . 17 𝑎[𝑑 / 𝑎]𝜑
8582, 83, 84nf3an 1902 . . . . . . . . . . . . . . . 16 𝑎(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)
8685nfex 2332 . . . . . . . . . . . . . . 15 𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)
87 opeq1 4767 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑑 → ⟨𝑎, 𝑏⟩ = ⟨𝑑, 𝑏⟩)
8887eqeq2d 2809 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑑 → (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩))
89 neeq1 3049 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑑 → (𝑎𝑏𝑑𝑏))
90 sbceq1a 3733 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑑 → (𝜑[𝑑 / 𝑎]𝜑))
9188, 89, 903anbi123d 1433 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑑 → ((⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)))
9291exbidv 1922 . . . . . . . . . . . . . . 15 (𝑎 = 𝑑 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)))
9381, 86, 92spcegf 3540 . . . . . . . . . . . . . 14 (𝑑𝑋 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑) → ∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
9435, 80, 93sylc 65 . . . . . . . . . . . . 13 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑))
95 vex 3445 . . . . . . . . . . . . . . . . . . . 20 𝑑 ∈ V
96 vex 3445 . . . . . . . . . . . . . . . . . . . 20 𝑐 ∈ V
9795, 96opth1 5336 . . . . . . . . . . . . . . . . . . 19 (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑑 = 𝑐)
9897equcomd 2026 . . . . . . . . . . . . . . . . . 18 (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑐 = 𝑑)
9998necon3ai 3012 . . . . . . . . . . . . . . . . 17 (𝑐𝑑 → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
10099adantl 485 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
101 eqeq2 2810 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
102101adantr 484 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑) → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
103100, 102mtbird 328 . . . . . . . . . . . . . . 15 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
1041033adant3 1129 . . . . . . . . . . . . . 14 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
105104adantl 485 . . . . . . . . . . . . 13 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
10694, 105jcnd 166 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
107 opeq1 4767 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑑 → ⟨𝑣, 𝑤⟩ = ⟨𝑑, 𝑤⟩)
108107eqeq1d 2800 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
1091083anbi1d 1437 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑑 → ((⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1101092exbidv 1925 . . . . . . . . . . . . . . 15 (𝑣 = 𝑑 → (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
111107eqeq1d 2800 . . . . . . . . . . . . . . 15 (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
112110, 111imbi12d 348 . . . . . . . . . . . . . 14 (𝑣 = 𝑑 → ((∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
113112notbid 321 . . . . . . . . . . . . 13 (𝑣 = 𝑑 → (¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
114 opeq2 4769 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑐 → ⟨𝑑, 𝑤⟩ = ⟨𝑑, 𝑐⟩)
115114eqeq1d 2800 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩))
1161153anbi1d 1437 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑐 → ((⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1171162exbidv 1925 . . . . . . . . . . . . . . 15 (𝑤 = 𝑐 → (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
118114eqeq1d 2800 . . . . . . . . . . . . . . 15 (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
119117, 118imbi12d 348 . . . . . . . . . . . . . 14 (𝑤 = 𝑐 → ((∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
120119notbid 321 . . . . . . . . . . . . 13 (𝑤 = 𝑐 → (¬ (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
121113, 120rspc2ev 3584 . . . . . . . . . . . 12 ((𝑑𝑋𝑐𝑋 ∧ ¬ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣𝑋𝑤𝑋 ¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
12235, 44, 106, 121syl3anc 1368 . . . . . . . . . . 11 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑣𝑋𝑤𝑋 ¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
123 rexnal2 3220 . . . . . . . . . . 11 (∃𝑣𝑋𝑤𝑋 ¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
124122, 123sylib 221 . . . . . . . . . 10 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
125124ex 416 . . . . . . . . 9 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
126125exlimdvv 1935 . . . . . . . 8 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∃𝑐𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
12723, 126syl5bi 245 . . . . . . 7 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
1281, 127syl5bir 246 . . . . . 6 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (¬ ¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
129128orrd 860 . . . . 5 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∨ ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
130 ianor 979 . . . . 5 (¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ (¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∨ ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
131129, 130sylibr 237 . . . 4 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
132131ralrimivva 3156 . . 3 ([𝑎𝑏]𝜑 → ∀𝑥𝑋𝑦𝑋 ¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
133 ralnex2 3222 . . 3 (∀𝑥𝑋𝑦𝑋 ¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ ¬ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
134132, 133sylib 221 . 2 ([𝑎𝑏]𝜑 → ¬ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
135 eqeq1 2802 . . . . 5 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
1361353anbi1d 1437 . . . 4 (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1371362exbidv 1925 . . 3 (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
138 eqeq1 2802 . . . . 5 (𝑝 = ⟨𝑣, 𝑤⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
1391383anbi1d 1437 . . . 4 (𝑝 = ⟨𝑣, 𝑤⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1401392exbidv 1925 . . 3 (𝑝 = ⟨𝑣, 𝑤⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
141137, 140reuop 6119 . 2 (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
142134, 141sylnibr 332 1 ([𝑎𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084  ∀wal 1536   = wceq 1538  ∃wex 1781  [wsb 2069   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  ∃!wreu 3108  [wsbc 3722  ⟨cop 4534   × cxp 5521  [wich 44130 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 2770  ax-sep 5171  ax-nul 5178  ax-pr 5299 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 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-opab 5097  df-xp 5529  df-ich 44131 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator