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

Theorem 2nreu 4339
 Description: If there are two different sets fulfilling a wff (by implicit substitution), then there is no unique set fulfilling the wff. (Contributed by AV, 20-Jun-2023.)
Hypotheses
Ref Expression
2nreu.a (𝑥 = 𝐴 → (𝜑𝜓))
2nreu.b (𝑥 = 𝐵 → (𝜑𝜒))
Assertion
Ref Expression
2nreu ((𝐴𝑋𝐵𝑋𝐴𝐵) → ((𝜓𝜒) → ¬ ∃!𝑥𝑋 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝑋   𝜒,𝑥   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 2nreu
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 simpl1 1189 . . . . . 6 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → 𝐴𝑋)
2 simpl2 1190 . . . . . 6 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → 𝐵𝑋)
3 simprl 771 . . . . . . 7 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → 𝜓)
4 2nreu.b . . . . . . . . . . . 12 (𝑥 = 𝐵 → (𝜑𝜒))
54sbcieg 3736 . . . . . . . . . . 11 (𝐵𝑋 → ([𝐵 / 𝑥]𝜑𝜒))
653ad2ant2 1132 . . . . . . . . . 10 ((𝐴𝑋𝐵𝑋𝐴𝐵) → ([𝐵 / 𝑥]𝜑𝜒))
76biimprd 251 . . . . . . . . 9 ((𝐴𝑋𝐵𝑋𝐴𝐵) → (𝜒[𝐵 / 𝑥]𝜑))
87adantld 495 . . . . . . . 8 ((𝐴𝑋𝐵𝑋𝐴𝐵) → ((𝜓𝜒) → [𝐵 / 𝑥]𝜑))
98imp 411 . . . . . . 7 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → [𝐵 / 𝑥]𝜑)
103, 9jca 516 . . . . . 6 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → (𝜓[𝐵 / 𝑥]𝜑))
11 simpl3 1191 . . . . . 6 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → 𝐴𝐵)
12 simp1 1134 . . . . . . 7 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → 𝐴𝑋)
13 simp2 1135 . . . . . . . . 9 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → 𝐵𝑋)
14 simp3 1136 . . . . . . . . . 10 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵))
15 sbcan 3746 . . . . . . . . . . . . . 14 ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥𝑦))
16 sbcan 3746 . . . . . . . . . . . . . . . 16 ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥][𝑦 / 𝑥]𝜑))
17 2nreu.a . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝐴 → (𝜑𝜓))
1817sbcieg 3736 . . . . . . . . . . . . . . . . 17 (𝐴𝑋 → ([𝐴 / 𝑥]𝜑𝜓))
19 nfs1v 2158 . . . . . . . . . . . . . . . . . 18 𝑥[𝑦 / 𝑥]𝜑
2019sbcgf 3769 . . . . . . . . . . . . . . . . 17 (𝐴𝑋 → ([𝐴 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
2118, 20anbi12d 634 . . . . . . . . . . . . . . . 16 (𝐴𝑋 → (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
2216, 21syl5bb 286 . . . . . . . . . . . . . . 15 (𝐴𝑋 → ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
23 sbcne12 4310 . . . . . . . . . . . . . . . 16 ([𝐴 / 𝑥]𝑥𝑦𝐴 / 𝑥𝑥𝐴 / 𝑥𝑦)
24 csbvarg 4329 . . . . . . . . . . . . . . . . 17 (𝐴𝑋𝐴 / 𝑥𝑥 = 𝐴)
25 csbconstg 3825 . . . . . . . . . . . . . . . . 17 (𝐴𝑋𝐴 / 𝑥𝑦 = 𝑦)
2624, 25neeq12d 3013 . . . . . . . . . . . . . . . 16 (𝐴𝑋 → (𝐴 / 𝑥𝑥𝐴 / 𝑥𝑦𝐴𝑦))
2723, 26syl5bb 286 . . . . . . . . . . . . . . 15 (𝐴𝑋 → ([𝐴 / 𝑥]𝑥𝑦𝐴𝑦))
2822, 27anbi12d 634 . . . . . . . . . . . . . 14 (𝐴𝑋 → (([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦)))
2915, 28syl5bb 286 . . . . . . . . . . . . 13 (𝐴𝑋 → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦)))
30293ad2ant1 1131 . . . . . . . . . . . 12 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦)))
3130sbcbidv 3752 . . . . . . . . . . 11 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ [𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦)))
32 sbcan 3746 . . . . . . . . . . . 12 ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦) ↔ ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴𝑦))
33 sbcan 3746 . . . . . . . . . . . . . 14 ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐵 / 𝑦]𝜓[𝐵 / 𝑦][𝑦 / 𝑥]𝜑))
34 sbcg 3771 . . . . . . . . . . . . . . . 16 (𝐵𝑋 → ([𝐵 / 𝑦]𝜓𝜓))
35 sbsbc 3701 . . . . . . . . . . . . . . . . . 18 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
3635sbcbii 3754 . . . . . . . . . . . . . . . . 17 ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑[𝐵 / 𝑦][𝑦 / 𝑥]𝜑)
37 sbccow 3720 . . . . . . . . . . . . . . . . . 18 ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑[𝐵 / 𝑥]𝜑)
3837a1i 11 . . . . . . . . . . . . . . . . 17 (𝐵𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
3936, 38syl5bb 286 . . . . . . . . . . . . . . . 16 (𝐵𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
4034, 39anbi12d 634 . . . . . . . . . . . . . . 15 (𝐵𝑋 → (([𝐵 / 𝑦]𝜓[𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓[𝐵 / 𝑥]𝜑)))
41403ad2ant2 1132 . . . . . . . . . . . . . 14 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → (([𝐵 / 𝑦]𝜓[𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓[𝐵 / 𝑥]𝜑)))
4233, 41syl5bb 286 . . . . . . . . . . . . 13 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓[𝐵 / 𝑥]𝜑)))
43 sbcne12 4310 . . . . . . . . . . . . . 14 ([𝐵 / 𝑦]𝐴𝑦𝐵 / 𝑦𝐴𝐵 / 𝑦𝑦)
44 csbconstg 3825 . . . . . . . . . . . . . . . 16 (𝐵𝑋𝐵 / 𝑦𝐴 = 𝐴)
45 csbvarg 4329 . . . . . . . . . . . . . . . 16 (𝐵𝑋𝐵 / 𝑦𝑦 = 𝐵)
4644, 45neeq12d 3013 . . . . . . . . . . . . . . 15 (𝐵𝑋 → (𝐵 / 𝑦𝐴𝐵 / 𝑦𝑦𝐴𝐵))
47463ad2ant2 1132 . . . . . . . . . . . . . 14 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → (𝐵 / 𝑦𝐴𝐵 / 𝑦𝑦𝐴𝐵))
4843, 47syl5bb 286 . . . . . . . . . . . . 13 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦]𝐴𝑦𝐴𝐵))
4942, 48anbi12d 634 . . . . . . . . . . . 12 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → (([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴𝑦) ↔ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)))
5032, 49syl5bb 286 . . . . . . . . . . 11 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴𝑦) ↔ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)))
5131, 50bitrd 282 . . . . . . . . . 10 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)))
5214, 51mpbird 260 . . . . . . . . 9 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → [𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
53 rspesbca 3788 . . . . . . . . 9 ((𝐵𝑋[𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦)) → ∃𝑦𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
5413, 52, 53syl2anc 588 . . . . . . . 8 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ∃𝑦𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
55 sbcrex 3782 . . . . . . . 8 ([𝐴 / 𝑥]𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦) ↔ ∃𝑦𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
5654, 55sylibr 237 . . . . . . 7 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → [𝐴 / 𝑥]𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
57 rspesbca 3788 . . . . . . 7 ((𝐴𝑋[𝐴 / 𝑥]𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦)) → ∃𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
5812, 56, 57syl2anc 588 . . . . . 6 ((𝐴𝑋𝐵𝑋 ∧ ((𝜓[𝐵 / 𝑥]𝜑) ∧ 𝐴𝐵)) → ∃𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
591, 2, 10, 11, 58syl112anc 1372 . . . . 5 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → ∃𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
60 pm4.61 409 . . . . . . 7 (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦))
61 df-ne 2953 . . . . . . . . 9 (𝑥𝑦 ↔ ¬ 𝑥 = 𝑦)
6261bicomi 227 . . . . . . . 8 𝑥 = 𝑦𝑥𝑦)
6362anbi2i 626 . . . . . . 7 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
6460, 63bitri 278 . . . . . 6 (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
65642rexbii 3177 . . . . 5 (∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥𝑦))
6659, 65sylibr 237 . . . 4 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
6766olcd 872 . . 3 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → (¬ ∃𝑥𝑋 𝜑 ∨ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
68 ianor 980 . . . . 5 (¬ (∃𝑥𝑋 𝜑 ∧ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥𝑋 𝜑 ∨ ¬ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
69 rexnal2 3185 . . . . . . 7 (∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
7069bicomi 227 . . . . . 6 (¬ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
7170orbi2i 911 . . . . 5 ((¬ ∃𝑥𝑋 𝜑 ∨ ¬ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥𝑋 𝜑 ∨ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
7268, 71bitri 278 . . . 4 (¬ (∃𝑥𝑋 𝜑 ∧ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥𝑋 𝜑 ∨ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
73 reu2 3640 . . . 4 (∃!𝑥𝑋 𝜑 ↔ (∃𝑥𝑋 𝜑 ∧ ∀𝑥𝑋𝑦𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
7472, 73xchnxbir 337 . . 3 (¬ ∃!𝑥𝑋 𝜑 ↔ (¬ ∃𝑥𝑋 𝜑 ∨ ∃𝑥𝑋𝑦𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
7567, 74sylibr 237 . 2 (((𝐴𝑋𝐵𝑋𝐴𝐵) ∧ (𝜓𝜒)) → ¬ ∃!𝑥𝑋 𝜑)
7675ex 417 1 ((𝐴𝑋𝐵𝑋𝐴𝐵) → ((𝜓𝜒) → ¬ ∃!𝑥𝑋 𝜑))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 845   ∧ w3a 1085   = wceq 1539  [wsb 2070   ∈ wcel 2112   ≠ wne 2952  ∀wral 3071  ∃wrex 3072  ∃!wreu 3073  [wsbc 3697  ⦋csb 3806 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 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  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-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-nul 4227 This theorem is referenced by:  reusq0  14863  addsqn2reu  26117  addsqrexnreu  26118  addsqnreup  26119  addsq2nreurex  26120
 Copyright terms: Public domain W3C validator