Proof of Theorem frege129d
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | frege129d.or | . 2
⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐴)) | 
| 2 |  | frege129d.f | . . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ V) | 
| 3 | 2 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → 𝐹 ∈ V) | 
| 4 |  | frege129d.a | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ dom 𝐹) | 
| 5 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → 𝐴 ∈ dom 𝐹) | 
| 6 |  | frege129d.c | . . . . . . . 8
⊢ (𝜑 → 𝐶 = (𝐹‘𝐴)) | 
| 7 | 6 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → 𝐶 = (𝐹‘𝐴)) | 
| 8 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → 𝐴(t+‘𝐹)𝐵) | 
| 9 |  | frege129d.fun | . . . . . . . 8
⊢ (𝜑 → Fun 𝐹) | 
| 10 | 9 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → Fun 𝐹) | 
| 11 | 3, 5, 7, 8, 10 | frege126d 43780 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → (𝐶(t+‘𝐹)𝐵 ∨ 𝐶 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐶)) | 
| 12 |  | biid 261 | . . . . . . 7
⊢ (𝐶(t+‘𝐹)𝐵 ↔ 𝐶(t+‘𝐹)𝐵) | 
| 13 |  | eqcom 2743 | . . . . . . 7
⊢ (𝐶 = 𝐵 ↔ 𝐵 = 𝐶) | 
| 14 |  | biid 261 | . . . . . . 7
⊢ (𝐵(t+‘𝐹)𝐶 ↔ 𝐵(t+‘𝐹)𝐶) | 
| 15 | 12, 13, 14 | 3orbi123i 1156 | . . . . . 6
⊢ ((𝐶(t+‘𝐹)𝐵 ∨ 𝐶 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐶) ↔ (𝐶(t+‘𝐹)𝐵 ∨ 𝐵 = 𝐶 ∨ 𝐵(t+‘𝐹)𝐶)) | 
| 16 | 11, 15 | sylib 218 | . . . . 5
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → (𝐶(t+‘𝐹)𝐵 ∨ 𝐵 = 𝐶 ∨ 𝐵(t+‘𝐹)𝐶)) | 
| 17 |  | 3orcomb 1093 | . . . . . 6
⊢ ((𝐶(t+‘𝐹)𝐵 ∨ 𝐵 = 𝐶 ∨ 𝐵(t+‘𝐹)𝐶) ↔ (𝐶(t+‘𝐹)𝐵 ∨ 𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶)) | 
| 18 |  | 3orrot 1091 | . . . . . 6
⊢ ((𝐶(t+‘𝐹)𝐵 ∨ 𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶) ↔ (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵)) | 
| 19 | 17, 18 | sylbb 219 | . . . . 5
⊢ ((𝐶(t+‘𝐹)𝐵 ∨ 𝐵 = 𝐶 ∨ 𝐵(t+‘𝐹)𝐶) → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵)) | 
| 20 | 16, 19 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵)) | 
| 21 | 20 | ex 412 | . . 3
⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵))) | 
| 22 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵) | 
| 23 | 6 | eqcomd 2742 | . . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) | 
| 24 |  | funbrfvb 6961 | . . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) = 𝐶 ↔ 𝐴𝐹𝐶)) | 
| 25 | 24 | biimpd 229 | . . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) = 𝐶 → 𝐴𝐹𝐶)) | 
| 26 | 9, 4, 25 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 → 𝐴𝐹𝐶)) | 
| 27 | 23, 26 | mpd 15 | . . . . . . . 8
⊢ (𝜑 → 𝐴𝐹𝐶) | 
| 28 | 2, 27 | frege91d 43769 | . . . . . . 7
⊢ (𝜑 → 𝐴(t+‘𝐹)𝐶) | 
| 29 | 28 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴(t+‘𝐹)𝐶) | 
| 30 | 22, 29 | eqbrtrrd 5166 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐵(t+‘𝐹)𝐶) | 
| 31 | 30 | ex 412 | . . . 4
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐵(t+‘𝐹)𝐶)) | 
| 32 |  | 3mix1 1330 | . . . 4
⊢ (𝐵(t+‘𝐹)𝐶 → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵)) | 
| 33 | 31, 32 | syl6 35 | . . 3
⊢ (𝜑 → (𝐴 = 𝐵 → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵))) | 
| 34 | 2 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐹 ∈ V) | 
| 35 |  | funrel 6582 | . . . . . . . . 9
⊢ (Fun
𝐹 → Rel 𝐹) | 
| 36 | 9, 35 | syl 17 | . . . . . . . 8
⊢ (𝜑 → Rel 𝐹) | 
| 37 |  | reltrclfv 15057 | . . . . . . . 8
⊢ ((𝐹 ∈ V ∧ Rel 𝐹) → Rel (t+‘𝐹)) | 
| 38 | 2, 36, 37 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → Rel (t+‘𝐹)) | 
| 39 |  | brrelex1 5737 | . . . . . . 7
⊢ ((Rel
(t+‘𝐹) ∧ 𝐵(t+‘𝐹)𝐴) → 𝐵 ∈ V) | 
| 40 | 38, 39 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐵 ∈ V) | 
| 41 |  | fvex 6918 | . . . . . . . 8
⊢ (𝐹‘𝐴) ∈ V | 
| 42 | 6, 41 | eqeltrdi 2848 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ V) | 
| 43 | 42 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐶 ∈ V) | 
| 44 | 4 | elexd 3503 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ V) | 
| 45 | 44 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐴 ∈ V) | 
| 46 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐵(t+‘𝐹)𝐴) | 
| 47 | 27 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐴𝐹𝐶) | 
| 48 | 34, 40, 43, 45, 46, 47 | frege96d 43767 | . . . . 5
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐵(t+‘𝐹)𝐶) | 
| 49 | 48 | ex 412 | . . . 4
⊢ (𝜑 → (𝐵(t+‘𝐹)𝐴 → 𝐵(t+‘𝐹)𝐶)) | 
| 50 | 49, 32 | syl6 35 | . . 3
⊢ (𝜑 → (𝐵(t+‘𝐹)𝐴 → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵))) | 
| 51 | 21, 33, 50 | 3jaod 1430 | . 2
⊢ (𝜑 → ((𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐴) → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵))) | 
| 52 | 1, 51 | mpd 15 | 1
⊢ (𝜑 → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵)) |