Users' Mathboxes 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 45654
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 314 . . . . . . 7 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ¬ ¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑))
2 nfv 1917 . . . . . . . . 9 𝑐(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)
3 nfv 1917 . . . . . . . . 9 𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)
4 nfv 1917 . . . . . . . . . 10 𝑎𝑥, 𝑦⟩ = ⟨𝑐, 𝑑
5 nfv 1917 . . . . . . . . . 10 𝑎 𝑐𝑑
6 nfsbc1v 3759 . . . . . . . . . 10 𝑎[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
74, 5, 6nf3an 1904 . . . . . . . . 9 𝑎(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
8 nfv 1917 . . . . . . . . . 10 𝑏𝑥, 𝑦⟩ = ⟨𝑐, 𝑑
9 nfv 1917 . . . . . . . . . 10 𝑏 𝑐𝑑
10 nfcv 2907 . . . . . . . . . . 11 𝑏𝑐
11 nfsbc1v 3759 . . . . . . . . . . 11 𝑏[𝑑 / 𝑏]𝜑
1210, 11nfsbcw 3761 . . . . . . . . . 10 𝑏[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
138, 9, 12nf3an 1904 . . . . . . . . 9 𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
14 opeq12 4832 . . . . . . . . . . 11 ((𝑎 = 𝑐𝑏 = 𝑑) → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)
1514eqeq2d 2747 . . . . . . . . . 10 ((𝑎 = 𝑐𝑏 = 𝑑) → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩))
16 simpl 483 . . . . . . . . . . 11 ((𝑎 = 𝑐𝑏 = 𝑑) → 𝑎 = 𝑐)
17 simpr 485 . . . . . . . . . . 11 ((𝑎 = 𝑐𝑏 = 𝑑) → 𝑏 = 𝑑)
1816, 17neeq12d 3005 . . . . . . . . . 10 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎𝑏𝑐𝑑))
19 sbceq1a 3750 . . . . . . . . . . 11 (𝑏 = 𝑑 → (𝜑[𝑑 / 𝑏]𝜑))
20 sbceq1a 3750 . . . . . . . . . . 11 (𝑎 = 𝑐 → ([𝑑 / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
2119, 20sylan9bbr 511 . . . . . . . . . 10 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
2215, 18, 213anbi123d 1436 . . . . . . . . 9 ((𝑎 = 𝑐𝑏 = 𝑑) → ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)))
232, 3, 7, 13, 22cbvex2v 2340 . . . . . . . 8 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑐𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
24 vex 3449 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
25 vex 3449 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
2624, 25opth 5433 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑥 = 𝑐𝑦 = 𝑑))
27 eleq1w 2820 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑑 → (𝑦𝑋𝑑𝑋))
2827biimpcd 248 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑋 → (𝑦 = 𝑑𝑑𝑋))
2928adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑋𝑦𝑋) → (𝑦 = 𝑑𝑑𝑋))
3029adantl 482 . . . . . . . . . . . . . . . . 17 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑦 = 𝑑𝑑𝑋))
3130com12 32 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
3231adantl 482 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
3326, 32sylbi 216 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
34333ad2ant1 1133 . . . . . . . . . . . . 13 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
3534impcom 408 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑𝑋)
36 eleq1w 2820 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑐 → (𝑥𝑋𝑐𝑋))
3736biimpcd 248 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑋 → (𝑥 = 𝑐𝑐𝑋))
3837adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑋𝑦𝑋) → (𝑥 = 𝑐𝑐𝑋))
3938adantl 482 . . . . . . . . . . . . . . . . 17 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 = 𝑐𝑐𝑋))
4039com12 32 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑐 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
4140adantr 481 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
4226, 41sylbi 216 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
43423ad2ant1 1133 . . . . . . . . . . . . 13 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
4443impcom 408 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑐𝑋)
45 eqidd 2737 . . . . . . . . . . . . . . . 16 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩)
46 necom 2997 . . . . . . . . . . . . . . . . . . 19 (𝑐𝑑𝑑𝑐)
4746biimpi 215 . . . . . . . . . . . . . . . . . 18 (𝑐𝑑𝑑𝑐)
48473ad2ant2 1134 . . . . . . . . . . . . . . . . 17 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → 𝑑𝑐)
4948adantl 482 . . . . . . . . . . . . . . . 16 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑𝑐)
50 dfich2 45640 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑎𝑏]𝜑 ↔ ∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
51 2sp 2179 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
52 sbsbc 3743 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑑 / 𝑏]𝜑[𝑑 / 𝑏]𝜑)
5352sbbii 2079 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
54 sbsbc 3743 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
5553, 54bitri 274 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
56 sbsbc 3743 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑐 / 𝑏]𝜑[𝑐 / 𝑏]𝜑)
5756sbbii 2079 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
58 sbsbc 3743 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
5957, 58bitri 274 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
6051, 55, 593bitr3g 312 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6160biimpd 228 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6250, 61sylbi 216 . . . . . . . . . . . . . . . . . . . . 21 ([𝑎𝑏]𝜑 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6362adantr 481 . . . . . . . . . . . . . . . . . . . 20 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6463com12 32 . . . . . . . . . . . . . . . . . . 19 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
65643ad2ant3 1135 . . . . . . . . . . . . . . . . . 18 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6665impcom 408 . . . . . . . . . . . . . . . . 17 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
67 sbccom 3827 . . . . . . . . . . . . . . . . 17 ([𝑐 / 𝑏][𝑑 / 𝑎]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
6866, 67sylibr 233 . . . . . . . . . . . . . . . 16 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
6945, 49, 683jca 1128 . . . . . . . . . . . . . . 15 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
70 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑏𝑑, 𝑐⟩ = ⟨𝑑, 𝑐
71 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑏 𝑑𝑐
72 nfsbc1v 3759 . . . . . . . . . . . . . . . . 17 𝑏[𝑐 / 𝑏][𝑑 / 𝑎]𝜑
7370, 71, 72nf3an 1904 . . . . . . . . . . . . . . . 16 𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
74 opeq2 4831 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑐 → ⟨𝑑, 𝑏⟩ = ⟨𝑑, 𝑐⟩)
7574eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑐 → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩))
76 neeq2 3007 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑐 → (𝑑𝑏𝑑𝑐))
77 sbceq1a 3750 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑐 → ([𝑑 / 𝑎]𝜑[𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
7875, 76, 773anbi123d 1436 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑐 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑)))
7910, 73, 78spcegf 3551 . . . . . . . . . . . . . . 15 (𝑐𝑋 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)))
8044, 69, 79sylc 65 . . . . . . . . . . . . . 14 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑))
81 nfcv 2907 . . . . . . . . . . . . . . 15 𝑎𝑑
82 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑎𝑑, 𝑐⟩ = ⟨𝑑, 𝑏
83 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑎 𝑑𝑏
84 nfsbc1v 3759 . . . . . . . . . . . . . . . . 17 𝑎[𝑑 / 𝑎]𝜑
8582, 83, 84nf3an 1904 . . . . . . . . . . . . . . . 16 𝑎(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)
8685nfex 2317 . . . . . . . . . . . . . . 15 𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)
87 opeq1 4830 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑑 → ⟨𝑎, 𝑏⟩ = ⟨𝑑, 𝑏⟩)
8887eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑑 → (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩))
89 neeq1 3006 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑑 → (𝑎𝑏𝑑𝑏))
90 sbceq1a 3750 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑑 → (𝜑[𝑑 / 𝑎]𝜑))
9188, 89, 903anbi123d 1436 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑑 → ((⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)))
9291exbidv 1924 . . . . . . . . . . . . . . 15 (𝑎 = 𝑑 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)))
9381, 86, 92spcegf 3551 . . . . . . . . . . . . . 14 (𝑑𝑋 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑) → ∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
9435, 80, 93sylc 65 . . . . . . . . . . . . 13 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑))
95 vex 3449 . . . . . . . . . . . . . . . . . . . 20 𝑑 ∈ V
96 vex 3449 . . . . . . . . . . . . . . . . . . . 20 𝑐 ∈ V
9795, 96opth1 5432 . . . . . . . . . . . . . . . . . . 19 (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑑 = 𝑐)
9897equcomd 2022 . . . . . . . . . . . . . . . . . 18 (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑐 = 𝑑)
9998necon3ai 2968 . . . . . . . . . . . . . . . . 17 (𝑐𝑑 → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
10099adantl 482 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
101 eqeq2 2748 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
102101adantr 481 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑) → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
103100, 102mtbird 324 . . . . . . . . . . . . . . 15 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
1041033adant3 1132 . . . . . . . . . . . . . 14 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
105104adantl 482 . . . . . . . . . . . . 13 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
10694, 105jcnd 163 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
107 opeq1 4830 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑑 → ⟨𝑣, 𝑤⟩ = ⟨𝑑, 𝑤⟩)
108107eqeq1d 2738 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
1091083anbi1d 1440 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑑 → ((⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1101092exbidv 1927 . . . . . . . . . . . . . . 15 (𝑣 = 𝑑 → (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
111107eqeq1d 2738 . . . . . . . . . . . . . . 15 (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
112110, 111imbi12d 344 . . . . . . . . . . . . . 14 (𝑣 = 𝑑 → ((∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
113112notbid 317 . . . . . . . . . . . . 13 (𝑣 = 𝑑 → (¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
114 opeq2 4831 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑐 → ⟨𝑑, 𝑤⟩ = ⟨𝑑, 𝑐⟩)
115114eqeq1d 2738 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩))
1161153anbi1d 1440 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑐 → ((⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1171162exbidv 1927 . . . . . . . . . . . . . . 15 (𝑤 = 𝑐 → (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
118114eqeq1d 2738 . . . . . . . . . . . . . . 15 (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
119117, 118imbi12d 344 . . . . . . . . . . . . . 14 (𝑤 = 𝑐 → ((∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
120119notbid 317 . . . . . . . . . . . . 13 (𝑤 = 𝑐 → (¬ (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
121113, 120rspc2ev 3592 . . . . . . . . . . . 12 ((𝑑𝑋𝑐𝑋 ∧ ¬ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣𝑋𝑤𝑋 ¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
12235, 44, 106, 121syl3anc 1371 . . . . . . . . . . 11 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑣𝑋𝑤𝑋 ¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
123 rexnal2 3132 . . . . . . . . . . 11 (∃𝑣𝑋𝑤𝑋 ¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
124122, 123sylib 217 . . . . . . . . . 10 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
125124ex 413 . . . . . . . . 9 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
126125exlimdvv 1937 . . . . . . . 8 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∃𝑐𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
12723, 126biimtrid 241 . . . . . . 7 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
1281, 127biimtrrid 242 . . . . . 6 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (¬ ¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
129128orrd 861 . . . . 5 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∨ ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
130 ianor 980 . . . . 5 (¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ (¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∨ ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
131129, 130sylibr 233 . . . 4 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
132131ralrimivva 3197 . . 3 ([𝑎𝑏]𝜑 → ∀𝑥𝑋𝑦𝑋 ¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
133 ralnex2 3130 . . 3 (∀𝑥𝑋𝑦𝑋 ¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ ¬ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
134132, 133sylib 217 . 2 ([𝑎𝑏]𝜑 → ¬ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
135 eqeq1 2740 . . . . 5 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
1361353anbi1d 1440 . . . 4 (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1371362exbidv 1927 . . 3 (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
138 eqeq1 2740 . . . . 5 (𝑝 = ⟨𝑣, 𝑤⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
1391383anbi1d 1440 . . . 4 (𝑝 = ⟨𝑣, 𝑤⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1401392exbidv 1927 . . 3 (𝑝 = ⟨𝑣, 𝑤⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
141137, 140reuop 6245 . 2 (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
142134, 141sylnibr 328 1 ([𝑎𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087  wal 1539   = wceq 1541  wex 1781  [wsb 2067  wcel 2106  wne 2943  wral 3064  wrex 3073  ∃!wreu 3351  [wsbc 3739  cop 4592   × cxp 5631  [wich 45627
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-opab 5168  df-xp 5639  df-ich 45628
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator