Proof of Theorem qliftfun
Step | Hyp | Ref
| Expression |
1 | | qlift.1 |
. . 3
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) |
2 | | qlift.2 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) |
3 | | qlift.3 |
. . . 4
⊢ (𝜑 → 𝑅 Er 𝑋) |
4 | | qlift.4 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ V) |
5 | 1, 2, 3, 4 | qliftlem 7715 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅 ∈ (𝑋 / 𝑅)) |
6 | | eceq1 7669 |
. . 3
⊢ (𝑥 = 𝑦 → [𝑥]𝑅 = [𝑦]𝑅) |
7 | | qliftfun.4 |
. . 3
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) |
8 | 1, 5, 2, 6, 7 | fliftfun 6462 |
. 2
⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵))) |
9 | 3 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑅 Er 𝑋) |
10 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥𝑅𝑦) |
11 | 9, 10 | ercl 7640 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝑋) |
12 | 9, 10 | ercl2 7642 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦 ∈ 𝑋) |
13 | 11, 12 | jca 553 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) |
14 | 13 | ex 449 |
. . . . . . . 8
⊢ (𝜑 → (𝑥𝑅𝑦 → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) |
15 | 14 | pm4.71rd 665 |
. . . . . . 7
⊢ (𝜑 → (𝑥𝑅𝑦 ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑅𝑦))) |
16 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑅 Er 𝑋) |
17 | | simprl 790 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) |
18 | 16, 17 | erth 7678 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ [𝑥]𝑅 = [𝑦]𝑅)) |
19 | 18 | pm5.32da 671 |
. . . . . . 7
⊢ (𝜑 → (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑅𝑦) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ [𝑥]𝑅 = [𝑦]𝑅))) |
20 | 15, 19 | bitrd 267 |
. . . . . 6
⊢ (𝜑 → (𝑥𝑅𝑦 ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ [𝑥]𝑅 = [𝑦]𝑅))) |
21 | 20 | imbi1d 330 |
. . . . 5
⊢ (𝜑 → ((𝑥𝑅𝑦 → 𝐴 = 𝐵) ↔ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ [𝑥]𝑅 = [𝑦]𝑅) → 𝐴 = 𝐵))) |
22 | | impexp 461 |
. . . . 5
⊢ ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ [𝑥]𝑅 = [𝑦]𝑅) → 𝐴 = 𝐵) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵))) |
23 | 21, 22 | syl6bb 275 |
. . . 4
⊢ (𝜑 → ((𝑥𝑅𝑦 → 𝐴 = 𝐵) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵)))) |
24 | 23 | 2albidv 1838 |
. . 3
⊢ (𝜑 → (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝐴 = 𝐵) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵)))) |
25 | | r2al 2923 |
. . 3
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵))) |
26 | 24, 25 | syl6bbr 277 |
. 2
⊢ (𝜑 → (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝐴 = 𝐵) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵))) |
27 | 8, 26 | bitr4d 270 |
1
⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝐴 = 𝐵))) |