Proof of Theorem reusv2lem5
Step | Hyp | Ref
| Expression |
1 | | tru 1487 |
. . . . . . . . 9
⊢
⊤ |
2 | | biimt 350 |
. . . . . . . . 9
⊢ ((𝐶 ∈ 𝐴 ∧ ⊤) → (𝑥 = 𝐶 ↔ ((𝐶 ∈ 𝐴 ∧ ⊤) → 𝑥 = 𝐶))) |
3 | 1, 2 | mpan2 707 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝐴 → (𝑥 = 𝐶 ↔ ((𝐶 ∈ 𝐴 ∧ ⊤) → 𝑥 = 𝐶))) |
4 | | ibar 525 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝐴 → (𝑥 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝑥 = 𝐶))) |
5 | 3, 4 | bitr3d 270 |
. . . . . . 7
⊢ (𝐶 ∈ 𝐴 → (((𝐶 ∈ 𝐴 ∧ ⊤) → 𝑥 = 𝐶) ↔ (𝐶 ∈ 𝐴 ∧ 𝑥 = 𝐶))) |
6 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) |
7 | 6 | pm5.32ri 670 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶) ↔ (𝐶 ∈ 𝐴 ∧ 𝑥 = 𝐶)) |
8 | 5, 7 | syl6bbr 278 |
. . . . . 6
⊢ (𝐶 ∈ 𝐴 → (((𝐶 ∈ 𝐴 ∧ ⊤) → 𝑥 = 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶))) |
9 | 8 | ralimi 2952 |
. . . . 5
⊢
(∀𝑦 ∈
𝐵 𝐶 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 (((𝐶 ∈ 𝐴 ∧ ⊤) → 𝑥 = 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶))) |
10 | | ralbi 3068 |
. . . . 5
⊢
(∀𝑦 ∈
𝐵 (((𝐶 ∈ 𝐴 ∧ ⊤) → 𝑥 = 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶)) → (∀𝑦 ∈ 𝐵 ((𝐶 ∈ 𝐴 ∧ ⊤) → 𝑥 = 𝐶) ↔ ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶))) |
11 | 9, 10 | syl 17 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 𝐶 ∈ 𝐴 → (∀𝑦 ∈ 𝐵 ((𝐶 ∈ 𝐴 ∧ ⊤) → 𝑥 = 𝐶) ↔ ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶))) |
12 | 11 | eubidv 2490 |
. . 3
⊢
(∀𝑦 ∈
𝐵 𝐶 ∈ 𝐴 → (∃!𝑥∀𝑦 ∈ 𝐵 ((𝐶 ∈ 𝐴 ∧ ⊤) → 𝑥 = 𝐶) ↔ ∃!𝑥∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶))) |
13 | | r19.28zv 4066 |
. . . 4
⊢ (𝐵 ≠ ∅ →
(∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 𝑥 = 𝐶))) |
14 | 13 | eubidv 2490 |
. . 3
⊢ (𝐵 ≠ ∅ →
(∃!𝑥∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 𝑥 = 𝐶))) |
15 | 12, 14 | sylan9bb 736 |
. 2
⊢
((∀𝑦 ∈
𝐵 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ ∅) → (∃!𝑥∀𝑦 ∈ 𝐵 ((𝐶 ∈ 𝐴 ∧ ⊤) → 𝑥 = 𝐶) ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 𝑥 = 𝐶))) |
16 | 1 | biantrur 527 |
. . . . 5
⊢ (𝑥 = 𝐶 ↔ (⊤ ∧ 𝑥 = 𝐶)) |
17 | 16 | rexbii 3041 |
. . . 4
⊢
(∃𝑦 ∈
𝐵 𝑥 = 𝐶 ↔ ∃𝑦 ∈ 𝐵 (⊤ ∧ 𝑥 = 𝐶)) |
18 | 17 | reubii 3128 |
. . 3
⊢
(∃!𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (⊤ ∧ 𝑥 = 𝐶)) |
19 | | reusv2lem4 4872 |
. . 3
⊢
(∃!𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 (⊤ ∧ 𝑥 = 𝐶) ↔ ∃!𝑥∀𝑦 ∈ 𝐵 ((𝐶 ∈ 𝐴 ∧ ⊤) → 𝑥 = 𝐶)) |
20 | 18, 19 | bitri 264 |
. 2
⊢
(∃!𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃!𝑥∀𝑦 ∈ 𝐵 ((𝐶 ∈ 𝐴 ∧ ⊤) → 𝑥 = 𝐶)) |
21 | | df-reu 2919 |
. 2
⊢
(∃!𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 𝑥 = 𝐶)) |
22 | 15, 20, 21 | 3bitr4g 303 |
1
⊢
((∀𝑦 ∈
𝐵 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 = 𝐶)) |