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
⊢ (𝜑 → 𝑋 ∈ 𝑉) | 
| 5 | 1, 2, 3, 4 | qliftlem 8838 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅 ∈ (𝑋 / 𝑅)) | 
| 6 |  | eceq1 8784 | . . 3
⊢ (𝑥 = 𝑦 → [𝑥]𝑅 = [𝑦]𝑅) | 
| 7 |  | qliftfun.4 | . . 3
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) | 
| 8 | 1, 5, 2, 6, 7 | fliftfun 7332 | . 2
⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵))) | 
| 9 | 3 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑅 Er 𝑋) | 
| 10 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥𝑅𝑦) | 
| 11 | 9, 10 | ercl 8756 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝑋) | 
| 12 | 9, 10 | ercl2 8758 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦 ∈ 𝑋) | 
| 13 | 11, 12 | jca 511 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) | 
| 14 | 13 | ex 412 | . . . . . . . 8
⊢ (𝜑 → (𝑥𝑅𝑦 → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) | 
| 15 | 14 | pm4.71rd 562 | . . . . . . 7
⊢ (𝜑 → (𝑥𝑅𝑦 ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑅𝑦))) | 
| 16 | 3 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑅 Er 𝑋) | 
| 17 |  | simprl 771 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) | 
| 18 | 16, 17 | erth 8796 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ [𝑥]𝑅 = [𝑦]𝑅)) | 
| 19 | 18 | pm5.32da 579 | . . . . . . 7
⊢ (𝜑 → (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑅𝑦) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ [𝑥]𝑅 = [𝑦]𝑅))) | 
| 20 | 15, 19 | bitrd 279 | . . . . . 6
⊢ (𝜑 → (𝑥𝑅𝑦 ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ [𝑥]𝑅 = [𝑦]𝑅))) | 
| 21 | 20 | imbi1d 341 | . . . . 5
⊢ (𝜑 → ((𝑥𝑅𝑦 → 𝐴 = 𝐵) ↔ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ [𝑥]𝑅 = [𝑦]𝑅) → 𝐴 = 𝐵))) | 
| 22 |  | impexp 450 | . . . . 5
⊢ ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ [𝑥]𝑅 = [𝑦]𝑅) → 𝐴 = 𝐵) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵))) | 
| 23 | 21, 22 | bitrdi 287 | . . . 4
⊢ (𝜑 → ((𝑥𝑅𝑦 → 𝐴 = 𝐵) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵)))) | 
| 24 | 23 | 2albidv 1923 | . . 3
⊢ (𝜑 → (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝐴 = 𝐵) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵)))) | 
| 25 |  | r2al 3195 | . . 3
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵))) | 
| 26 | 24, 25 | bitr4di 289 | . 2
⊢ (𝜑 → (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝐴 = 𝐵) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ([𝑥]𝑅 = [𝑦]𝑅 → 𝐴 = 𝐵))) | 
| 27 | 8, 26 | bitr4d 282 | 1
⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝐴 = 𝐵))) |