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 44597
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 1922 . . . . . . . . 9 𝑐(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)
3 nfv 1922 . . . . . . . . 9 𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)
4 nfv 1922 . . . . . . . . . 10 𝑎𝑥, 𝑦⟩ = ⟨𝑐, 𝑑
5 nfv 1922 . . . . . . . . . 10 𝑎 𝑐𝑑
6 nfsbc1v 3714 . . . . . . . . . 10 𝑎[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
74, 5, 6nf3an 1909 . . . . . . . . 9 𝑎(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
8 nfv 1922 . . . . . . . . . 10 𝑏𝑥, 𝑦⟩ = ⟨𝑐, 𝑑
9 nfv 1922 . . . . . . . . . 10 𝑏 𝑐𝑑
10 nfcv 2904 . . . . . . . . . . 11 𝑏𝑐
11 nfsbc1v 3714 . . . . . . . . . . 11 𝑏[𝑑 / 𝑏]𝜑
1210, 11nfsbcw 3716 . . . . . . . . . 10 𝑏[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
138, 9, 12nf3an 1909 . . . . . . . . 9 𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
14 opeq12 4786 . . . . . . . . . . 11 ((𝑎 = 𝑐𝑏 = 𝑑) → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)
1514eqeq2d 2748 . . . . . . . . . 10 ((𝑎 = 𝑐𝑏 = 𝑑) → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩))
16 simpl 486 . . . . . . . . . . 11 ((𝑎 = 𝑐𝑏 = 𝑑) → 𝑎 = 𝑐)
17 simpr 488 . . . . . . . . . . 11 ((𝑎 = 𝑐𝑏 = 𝑑) → 𝑏 = 𝑑)
1816, 17neeq12d 3002 . . . . . . . . . 10 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎𝑏𝑐𝑑))
19 sbceq1a 3705 . . . . . . . . . . 11 (𝑏 = 𝑑 → (𝜑[𝑑 / 𝑏]𝜑))
20 sbceq1a 3705 . . . . . . . . . . 11 (𝑎 = 𝑐 → ([𝑑 / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
2119, 20sylan9bbr 514 . . . . . . . . . 10 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
2215, 18, 213anbi123d 1438 . . . . . . . . 9 ((𝑎 = 𝑐𝑏 = 𝑑) → ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)))
232, 3, 7, 13, 22cbvex2v 2345 . . . . . . . 8 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑐𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
24 vex 3412 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
25 vex 3412 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
2624, 25opth 5360 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑥 = 𝑐𝑦 = 𝑑))
27 eleq1w 2820 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑑 → (𝑦𝑋𝑑𝑋))
2827biimpcd 252 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑋 → (𝑦 = 𝑑𝑑𝑋))
2928adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑋𝑦𝑋) → (𝑦 = 𝑑𝑑𝑋))
3029adantl 485 . . . . . . . . . . . . . . . . 17 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑦 = 𝑑𝑑𝑋))
3130com12 32 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
3231adantl 485 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
3326, 32sylbi 220 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
34333ad2ant1 1135 . . . . . . . . . . . . 13 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑑𝑋))
3534impcom 411 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑𝑋)
36 eleq1w 2820 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑐 → (𝑥𝑋𝑐𝑋))
3736biimpcd 252 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑋 → (𝑥 = 𝑐𝑐𝑋))
3837adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑋𝑦𝑋) → (𝑥 = 𝑐𝑐𝑋))
3938adantl 485 . . . . . . . . . . . . . . . . 17 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 = 𝑐𝑐𝑋))
4039com12 32 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑐 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
4140adantr 484 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
4226, 41sylbi 220 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
43423ad2ant1 1135 . . . . . . . . . . . . 13 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑐𝑋))
4443impcom 411 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑐𝑋)
45 eqidd 2738 . . . . . . . . . . . . . . . 16 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩)
46 necom 2994 . . . . . . . . . . . . . . . . . . 19 (𝑐𝑑𝑑𝑐)
4746biimpi 219 . . . . . . . . . . . . . . . . . 18 (𝑐𝑑𝑑𝑐)
48473ad2ant2 1136 . . . . . . . . . . . . . . . . 17 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → 𝑑𝑐)
4948adantl 485 . . . . . . . . . . . . . . . 16 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑𝑐)
50 dfich2 44583 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑎𝑏]𝜑 ↔ ∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
51 2sp 2183 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
52 sbsbc 3698 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑑 / 𝑏]𝜑[𝑑 / 𝑏]𝜑)
5352sbbii 2082 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
54 sbsbc 3698 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
5553, 54bitri 278 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
56 sbsbc 3698 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑐 / 𝑏]𝜑[𝑐 / 𝑏]𝜑)
5756sbbii 2082 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
58 sbsbc 3698 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
5957, 58bitri 278 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
6051, 55, 593bitr3g 316 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6160biimpd 232 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑐𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6250, 61sylbi 220 . . . . . . . . . . . . . . . . . . . . 21 ([𝑎𝑏]𝜑 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6362adantr 484 . . . . . . . . . . . . . . . . . . . 20 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6463com12 32 . . . . . . . . . . . . . . . . . . 19 ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
65643ad2ant3 1137 . . . . . . . . . . . . . . . . . 18 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
6665impcom 411 . . . . . . . . . . . . . . . . 17 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
67 sbccom 3783 . . . . . . . . . . . . . . . . 17 ([𝑐 / 𝑏][𝑑 / 𝑎]𝜑[𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
6866, 67sylibr 237 . . . . . . . . . . . . . . . 16 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
6945, 49, 683jca 1130 . . . . . . . . . . . . . . 15 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
70 nfv 1922 . . . . . . . . . . . . . . . . 17 𝑏𝑑, 𝑐⟩ = ⟨𝑑, 𝑐
71 nfv 1922 . . . . . . . . . . . . . . . . 17 𝑏 𝑑𝑐
72 nfsbc1v 3714 . . . . . . . . . . . . . . . . 17 𝑏[𝑐 / 𝑏][𝑑 / 𝑎]𝜑
7370, 71, 72nf3an 1909 . . . . . . . . . . . . . . . 16 𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
74 opeq2 4785 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑐 → ⟨𝑑, 𝑏⟩ = ⟨𝑑, 𝑐⟩)
7574eqeq2d 2748 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑐 → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩))
76 neeq2 3004 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑐 → (𝑑𝑏𝑑𝑐))
77 sbceq1a 3705 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑐 → ([𝑑 / 𝑎]𝜑[𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
7875, 76, 773anbi123d 1438 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑐 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑)))
7910, 73, 78spcegf 3507 . . . . . . . . . . . . . . 15 (𝑐𝑋 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑𝑐[𝑐 / 𝑏][𝑑 / 𝑎]𝜑) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)))
8044, 69, 79sylc 65 . . . . . . . . . . . . . 14 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑))
81 nfcv 2904 . . . . . . . . . . . . . . 15 𝑎𝑑
82 nfv 1922 . . . . . . . . . . . . . . . . 17 𝑎𝑑, 𝑐⟩ = ⟨𝑑, 𝑏
83 nfv 1922 . . . . . . . . . . . . . . . . 17 𝑎 𝑑𝑏
84 nfsbc1v 3714 . . . . . . . . . . . . . . . . 17 𝑎[𝑑 / 𝑎]𝜑
8582, 83, 84nf3an 1909 . . . . . . . . . . . . . . . 16 𝑎(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)
8685nfex 2323 . . . . . . . . . . . . . . 15 𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)
87 opeq1 4784 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑑 → ⟨𝑎, 𝑏⟩ = ⟨𝑑, 𝑏⟩)
8887eqeq2d 2748 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑑 → (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩))
89 neeq1 3003 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑑 → (𝑎𝑏𝑑𝑏))
90 sbceq1a 3705 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑑 → (𝜑[𝑑 / 𝑎]𝜑))
9188, 89, 903anbi123d 1438 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑑 → ((⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)))
9291exbidv 1929 . . . . . . . . . . . . . . 15 (𝑎 = 𝑑 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑)))
9381, 86, 92spcegf 3507 . . . . . . . . . . . . . 14 (𝑑𝑋 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑𝑏[𝑑 / 𝑎]𝜑) → ∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
9435, 80, 93sylc 65 . . . . . . . . . . . . 13 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑))
95 vex 3412 . . . . . . . . . . . . . . . . . . . 20 𝑑 ∈ V
96 vex 3412 . . . . . . . . . . . . . . . . . . . 20 𝑐 ∈ V
9795, 96opth1 5359 . . . . . . . . . . . . . . . . . . 19 (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑑 = 𝑐)
9897equcomd 2027 . . . . . . . . . . . . . . . . . 18 (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑐 = 𝑑)
9998necon3ai 2965 . . . . . . . . . . . . . . . . 17 (𝑐𝑑 → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
10099adantl 485 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
101 eqeq2 2749 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
102101adantr 484 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑) → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
103100, 102mtbird 328 . . . . . . . . . . . . . . 15 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
1041033adant3 1134 . . . . . . . . . . . . . 14 ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
105104adantl 485 . . . . . . . . . . . . 13 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
10694, 105jcnd 166 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
107 opeq1 4784 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑑 → ⟨𝑣, 𝑤⟩ = ⟨𝑑, 𝑤⟩)
108107eqeq1d 2739 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
1091083anbi1d 1442 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑑 → ((⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1101092exbidv 1932 . . . . . . . . . . . . . . 15 (𝑣 = 𝑑 → (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
111107eqeq1d 2739 . . . . . . . . . . . . . . 15 (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
112110, 111imbi12d 348 . . . . . . . . . . . . . 14 (𝑣 = 𝑑 → ((∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
113112notbid 321 . . . . . . . . . . . . 13 (𝑣 = 𝑑 → (¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
114 opeq2 4785 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑐 → ⟨𝑑, 𝑤⟩ = ⟨𝑑, 𝑐⟩)
115114eqeq1d 2739 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩))
1161153anbi1d 1442 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑐 → ((⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1171162exbidv 1932 . . . . . . . . . . . . . . 15 (𝑤 = 𝑐 → (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
118114eqeq1d 2739 . . . . . . . . . . . . . . 15 (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
119117, 118imbi12d 348 . . . . . . . . . . . . . 14 (𝑤 = 𝑐 → ((∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
120119notbid 321 . . . . . . . . . . . . 13 (𝑤 = 𝑐 → (¬ (∃𝑎𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
121113, 120rspc2ev 3549 . . . . . . . . . . . 12 ((𝑑𝑋𝑐𝑋 ∧ ¬ (∃𝑎𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣𝑋𝑤𝑋 ¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
12235, 44, 106, 121syl3anc 1373 . . . . . . . . . . 11 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑣𝑋𝑤𝑋 ¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
123 rexnal2 3179 . . . . . . . . . . 11 (∃𝑣𝑋𝑤𝑋 ¬ (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
124122, 123sylib 221 . . . . . . . . . 10 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
125124ex 416 . . . . . . . . 9 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
126125exlimdvv 1942 . . . . . . . 8 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∃𝑐𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐𝑑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
12723, 126syl5bi 245 . . . . . . 7 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
1281, 127syl5bir 246 . . . . . 6 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (¬ ¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
129128orrd 863 . . . . 5 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∨ ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
130 ianor 982 . . . . 5 (¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ (¬ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∨ ¬ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
131129, 130sylibr 237 . . . 4 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
132131ralrimivva 3112 . . 3 ([𝑎𝑏]𝜑 → ∀𝑥𝑋𝑦𝑋 ¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
133 ralnex2 3181 . . 3 (∀𝑥𝑋𝑦𝑋 ¬ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ ¬ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
134132, 133sylib 221 . 2 ([𝑎𝑏]𝜑 → ¬ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
135 eqeq1 2741 . . . . 5 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
1361353anbi1d 1442 . . . 4 (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1371362exbidv 1932 . . 3 (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
138 eqeq1 2741 . . . . 5 (𝑝 = ⟨𝑣, 𝑤⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
1391383anbi1d 1442 . . . 4 (𝑝 = ⟨𝑣, 𝑤⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
1401392exbidv 1932 . . 3 (𝑝 = ⟨𝑣, 𝑤⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑)))
141137, 140reuop 6156 . 2 (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ↔ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
142134, 141sylnibr 332 1 ([𝑎𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎𝑏𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847  w3a 1089  wal 1541   = wceq 1543  wex 1787  [wsb 2070  wcel 2110  wne 2940  wral 3061  wrex 3062  ∃!wreu 3063  [wsbc 3694  cop 4547   × cxp 5549  [wich 44570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-opab 5116  df-xp 5557  df-ich 44571
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator