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 44893
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 315 . . . . . . 7 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ¬ ¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑))
2 nfv 1921 . . . . . . . . 9 𝑐(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)
3 nfv 1921 . . . . . . . . 9 𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)
4 nfv 1921 . . . . . . . . . 10 𝑎𝑥, 𝑦⟩ = ⟨𝑐, 𝑑
5 nfv 1921 . . . . . . . . . 10 𝑎 𝑐𝑑
6 nfsbc1v 3740 . . . . . . . . . 10 𝑎[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
74, 5, 6nf3an 1908 . . . . . . . . 9 𝑎(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
8 nfv 1921 . . . . . . . . . 10 𝑏𝑥, 𝑦⟩ = ⟨𝑐, 𝑑
9 nfv 1921 . . . . . . . . . 10 𝑏 𝑐𝑑
10 nfcv 2909 . . . . . . . . . . 11 𝑏𝑐
11 nfsbc1v 3740 . . . . . . . . . . 11 𝑏[𝑑 / 𝑏]𝜑
1210, 11nfsbcw 3742 . . . . . . . . . 10 𝑏[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
138, 9, 12nf3an 1908 . . . . . . . . 9 𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
14 opeq12 4812 . . . . . . . . . . 11 ((𝑎 = 𝑐𝑏 = 𝑑) → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)
1514eqeq2d 2751 . . . . . . . . . 10 ((𝑎 = 𝑐𝑏 = 𝑑) → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩))
16 simpl 483 . . . . . . . . . . 11 ((𝑎 = 𝑐𝑏 = 𝑑) → 𝑎 = 𝑐)
17 simpr 485 . . . . . . . . . . 11 ((𝑎 = 𝑐𝑏 = 𝑑) → 𝑏 = 𝑑)
1816, 17neeq12d 3007 . . . . . . . . . 10 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎𝑏𝑐𝑑))
19 sbceq1a 3731 . . . . . . . . . . 11 (𝑏 = 𝑑 → (𝜑[𝑑 / 𝑏]𝜑))
20 sbceq1a 3731 . . . . . . . . . . 11 (𝑎 = 𝑐 → ([𝑑 / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
2119, 20sylan9bbr 511 . . . . . . . . . 10 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
2215, 18, 213anbi123d 1435 . . . . . . . . 9 ((𝑎 = 𝑐𝑏 = 𝑑) → ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)))
232, 3, 7, 13, 22cbvex2v 2346 . . . . . . . 8 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑐𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
24 vex 3435 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
25 vex 3435 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
2624, 25opth 5395 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑥 = 𝑐𝑦 = 𝑑))
27 eleq1w 2823 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑑 → (𝑦𝑋𝑑𝑋))
2827biimpcd 248 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑋 → (𝑦 = 𝑑𝑑𝑋))
2928adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑋𝑦𝑋) → (𝑦 = 𝑑𝑑𝑋))
3029adantl 482 . . . . . . . . . . . . . . . . 17 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑦 = 𝑑𝑑𝑋))
3130com12 32 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
3231adantl 482 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
3326, 32sylbi 216 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
34333ad2ant1 1132 . . . . . . . . . . . . 13 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
3534impcom 408 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑𝑋)
36 eleq1w 2823 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑐 → (𝑥𝑋𝑐𝑋))
3736biimpcd 248 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑋 → (𝑥 = 𝑐𝑐𝑋))
3837adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑋𝑦𝑋) → (𝑥 = 𝑐𝑐𝑋))
3938adantl 482 . . . . . . . . . . . . . . . . 17 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 = 𝑐𝑐𝑋))
4039com12 32 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑐 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
4140adantr 481 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
4226, 41sylbi 216 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
43423ad2ant1 1132 . . . . . . . . . . . . 13 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
4443impcom 408 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑐𝑋)
45 eqidd 2741 . . . . . . . . . . . . . . . 16 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩)
46 necom 2999 . . . . . . . . . . . . . . . . . . 19 (𝑐𝑑𝑑𝑐)
4746biimpi 215 . . . . . . . . . . . . . . . . . 18 (𝑐𝑑𝑑𝑐)
48473ad2ant2 1133 . . . . . . . . . . . . . . . . 17 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → 𝑑𝑐)
4948adantl 482 . . . . . . . . . . . . . . . 16 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑𝑐)
50 dfich2 44879 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑎𝑏]𝜑 ↔ ∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
51 2sp 2183 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
52 sbsbc 3724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑑 / 𝑏]𝜑[𝑑 / 𝑏]𝜑)
5352sbbii 2083 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
54 sbsbc 3724 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
5553, 54bitri 274 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
56 sbsbc 3724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑐 / 𝑏]𝜑[𝑐 / 𝑏]𝜑)
5756sbbii 2083 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
58 sbsbc 3724 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
5957, 58bitri 274 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
6051, 55, 593bitr3g 313 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6160biimpd 228 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6250, 61sylbi 216 . . . . . . . . . . . . . . . . . . . . 21 ([𝑎𝑏]𝜑 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6362adantr 481 . . . . . . . . . . . . . . . . . . . 20 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6463com12 32 . . . . . . . . . . . . . . . . . . 19 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
65643ad2ant3 1134 . . . . . . . . . . . . . . . . . 18 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6665impcom 408 . . . . . . . . . . . . . . . . 17 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
67 sbccom 3809 . . . . . . . . . . . . . . . . 17 ([𝑐 / 𝑏][𝑑 / 𝑎]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
6866, 67sylibr 233 . . . . . . . . . . . . . . . 16 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
6945, 49, 683jca 1127 . . . . . . . . . . . . . . 15 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
70 nfv 1921 . . . . . . . . . . . . . . . . 17 𝑏𝑑, 𝑐⟩ = ⟨𝑑, 𝑐
71 nfv 1921 . . . . . . . . . . . . . . . . 17 𝑏 𝑑𝑐
72 nfsbc1v 3740 . . . . . . . . . . . . . . . . 17 𝑏[𝑐 / 𝑏][𝑑 / 𝑎]𝜑
7370, 71, 72nf3an 1908 . . . . . . . . . . . . . . . 16 𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
74 opeq2 4811 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑐 → ⟨𝑑, 𝑏⟩ = ⟨𝑑, 𝑐⟩)
7574eqeq2d 2751 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑐 → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩))
76 neeq2 3009 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑐 → (𝑑𝑏𝑑𝑐))
77 sbceq1a 3731 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑐 → ([𝑑 / 𝑎]𝜑[𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
7875, 76, 773anbi123d 1435 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑐 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑)))
7910, 73, 78spcegf 3530 . . . . . . . . . . . . . . 15 (𝑐𝑋 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)))
8044, 69, 79sylc 65 . . . . . . . . . . . . . 14 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑))
81 nfcv 2909 . . . . . . . . . . . . . . 15 𝑎𝑑
82 nfv 1921 . . . . . . . . . . . . . . . . 17 𝑎𝑑, 𝑐⟩ = ⟨𝑑, 𝑏
83 nfv 1921 . . . . . . . . . . . . . . . . 17 𝑎 𝑑𝑏
84 nfsbc1v 3740 . . . . . . . . . . . . . . . . 17 𝑎[𝑑 / 𝑎]𝜑
8582, 83, 84nf3an 1908 . . . . . . . . . . . . . . . 16 𝑎(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)
8685nfex 2322 . . . . . . . . . . . . . . 15 𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)
87 opeq1 4810 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑑 → ⟨𝑎, 𝑏⟩ = ⟨𝑑, 𝑏⟩)
8887eqeq2d 2751 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑑 → (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩))
89 neeq1 3008 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑑 → (𝑎𝑏𝑑𝑏))
90 sbceq1a 3731 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑑 → (𝜑[𝑑 / 𝑎]𝜑))
9188, 89, 903anbi123d 1435 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑑 → ((⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)))
9291exbidv 1928 . . . . . . . . . . . . . . 15 (𝑎 = 𝑑 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)))
9381, 86, 92spcegf 3530 . . . . . . . . . . . . . 14 (𝑑𝑋 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑) → ∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
9435, 80, 93sylc 65 . . . . . . . . . . . . 13 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑))
95 vex 3435 . . . . . . . . . . . . . . . . . . . 20 𝑑 ∈ V
96 vex 3435 . . . . . . . . . . . . . . . . . . . 20 𝑐 ∈ V
9795, 96opth1 5394 . . . . . . . . . . . . . . . . . . 19 (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑑 = 𝑐)
9897equcomd 2026 . . . . . . . . . . . . . . . . . 18 (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑐 = 𝑑)
9998necon3ai 2970 . . . . . . . . . . . . . . . . 17 (𝑐𝑑 → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
10099adantl 482 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
101 eqeq2 2752 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
102101adantr 481 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑) → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
103100, 102mtbird 325 . . . . . . . . . . . . . . 15 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
1041033adant3 1131 . . . . . . . . . . . . . 14 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
105104adantl 482 . . . . . . . . . . . . 13 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
10694, 105jcnd 163 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
107 opeq1 4810 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑑 → ⟨𝑣, 𝑤⟩ = ⟨𝑑, 𝑤⟩)
108107eqeq1d 2742 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
1091083anbi1d 1439 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑑 → ((⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1101092exbidv 1931 . . . . . . . . . . . . . . 15 (𝑣 = 𝑑 → (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
111107eqeq1d 2742 . . . . . . . . . . . . . . 15 (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
112110, 111imbi12d 345 . . . . . . . . . . . . . 14 (𝑣 = 𝑑 → ((∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
113112notbid 318 . . . . . . . . . . . . 13 (𝑣 = 𝑑 → (¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
114 opeq2 4811 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑐 → ⟨𝑑, 𝑤⟩ = ⟨𝑑, 𝑐⟩)
115114eqeq1d 2742 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩))
1161153anbi1d 1439 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑐 → ((⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1171162exbidv 1931 . . . . . . . . . . . . . . 15 (𝑤 = 𝑐 → (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
118114eqeq1d 2742 . . . . . . . . . . . . . . 15 (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
119117, 118imbi12d 345 . . . . . . . . . . . . . 14 (𝑤 = 𝑐 → ((∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
120119notbid 318 . . . . . . . . . . . . 13 (𝑤 = 𝑐 → (¬ (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
121113, 120rspc2ev 3573 . . . . . . . . . . . 12 ((𝑑𝑋𝑐𝑋 ∧ ¬ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣𝑋𝑤𝑋 ¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
12235, 44, 106, 121syl3anc 1370 . . . . . . . . . . 11 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑣𝑋𝑤𝑋 ¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
123 rexnal2 3189 . . . . . . . . . . 11 (∃𝑣𝑋𝑤𝑋 ¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
124122, 123sylib 217 . . . . . . . . . 10 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
125124ex 413 . . . . . . . . 9 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
126125exlimdvv 1941 . . . . . . . 8 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∃𝑐𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
12723, 126syl5bi 241 . . . . . . 7 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
1281, 127syl5bir 242 . . . . . 6 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (¬ ¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
129128orrd 860 . . . . 5 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∨ ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
130 ianor 979 . . . . 5 (¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ (¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∨ ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
131129, 130sylibr 233 . . . 4 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
132131ralrimivva 3117 . . 3 ([𝑎𝑏]𝜑 → ∀𝑥𝑋𝑦𝑋 ¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
133 ralnex2 3191 . . 3 (∀𝑥𝑋𝑦𝑋 ¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ ¬ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
134132, 133sylib 217 . 2 ([𝑎𝑏]𝜑 → ¬ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
135 eqeq1 2744 . . . . 5 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
1361353anbi1d 1439 . . . 4 (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1371362exbidv 1931 . . 3 (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
138 eqeq1 2744 . . . . 5 (𝑝 = ⟨𝑣, 𝑤⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
1391383anbi1d 1439 . . . 4 (𝑝 = ⟨𝑣, 𝑤⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1401392exbidv 1931 . . 3 (𝑝 = ⟨𝑣, 𝑤⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
141137, 140reuop 6195 . 2 (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
142134, 141sylnibr 329 1 ([𝑎𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3a 1086  wal 1540   = wceq 1542  wex 1786  [wsb 2071  wcel 2110  wne 2945  wral 3066  wrex 3067  ∃!wreu 3068  [wsbc 3720  cop 4573   × cxp 5588  [wich 44866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5142  df-xp 5596  df-ich 44867
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator