Proof of Theorem frege129d
Step | Hyp | Ref
| Expression |
1 | | frege129d.or |
. 2
⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐴)) |
2 | | frege129d.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ V) |
3 | 2 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → 𝐹 ∈ V) |
4 | | frege129d.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ dom 𝐹) |
5 | 4 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → 𝐴 ∈ dom 𝐹) |
6 | | frege129d.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 = (𝐹‘𝐴)) |
7 | 6 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → 𝐶 = (𝐹‘𝐴)) |
8 | | simpr 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → 𝐴(t+‘𝐹)𝐵) |
9 | | frege129d.fun |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐹) |
10 | 9 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → Fun 𝐹) |
11 | 3, 5, 7, 8, 10 | frege126d 40114 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → (𝐶(t+‘𝐹)𝐵 ∨ 𝐶 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐶)) |
12 | | biid 263 |
. . . . . . 7
⊢ (𝐶(t+‘𝐹)𝐵 ↔ 𝐶(t+‘𝐹)𝐵) |
13 | | eqcom 2830 |
. . . . . . 7
⊢ (𝐶 = 𝐵 ↔ 𝐵 = 𝐶) |
14 | | biid 263 |
. . . . . . 7
⊢ (𝐵(t+‘𝐹)𝐶 ↔ 𝐵(t+‘𝐹)𝐶) |
15 | 12, 13, 14 | 3orbi123i 1152 |
. . . . . 6
⊢ ((𝐶(t+‘𝐹)𝐵 ∨ 𝐶 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐶) ↔ (𝐶(t+‘𝐹)𝐵 ∨ 𝐵 = 𝐶 ∨ 𝐵(t+‘𝐹)𝐶)) |
16 | 11, 15 | sylib 220 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → (𝐶(t+‘𝐹)𝐵 ∨ 𝐵 = 𝐶 ∨ 𝐵(t+‘𝐹)𝐶)) |
17 | | 3orcomb 1090 |
. . . . . 6
⊢ ((𝐶(t+‘𝐹)𝐵 ∨ 𝐵 = 𝐶 ∨ 𝐵(t+‘𝐹)𝐶) ↔ (𝐶(t+‘𝐹)𝐵 ∨ 𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶)) |
18 | | 3orrot 1088 |
. . . . . 6
⊢ ((𝐶(t+‘𝐹)𝐵 ∨ 𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶) ↔ (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵)) |
19 | 17, 18 | sylbb 221 |
. . . . 5
⊢ ((𝐶(t+‘𝐹)𝐵 ∨ 𝐵 = 𝐶 ∨ 𝐵(t+‘𝐹)𝐶) → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵)) |
20 | 16, 19 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐴(t+‘𝐹)𝐵) → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵)) |
21 | 20 | ex 415 |
. . 3
⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵))) |
22 | | simpr 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵) |
23 | 6 | eqcomd 2829 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) |
24 | | funbrfvb 6722 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) = 𝐶 ↔ 𝐴𝐹𝐶)) |
25 | 24 | biimpd 231 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) = 𝐶 → 𝐴𝐹𝐶)) |
26 | 9, 4, 25 | syl2anc 586 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 → 𝐴𝐹𝐶)) |
27 | 23, 26 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → 𝐴𝐹𝐶) |
28 | 2, 27 | frege91d 40103 |
. . . . . . 7
⊢ (𝜑 → 𝐴(t+‘𝐹)𝐶) |
29 | 28 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴(t+‘𝐹)𝐶) |
30 | 22, 29 | eqbrtrrd 5092 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐵(t+‘𝐹)𝐶) |
31 | 30 | ex 415 |
. . . 4
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐵(t+‘𝐹)𝐶)) |
32 | | 3mix1 1326 |
. . . 4
⊢ (𝐵(t+‘𝐹)𝐶 → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵)) |
33 | 31, 32 | syl6 35 |
. . 3
⊢ (𝜑 → (𝐴 = 𝐵 → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵))) |
34 | 2 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐹 ∈ V) |
35 | | funrel 6374 |
. . . . . . . . 9
⊢ (Fun
𝐹 → Rel 𝐹) |
36 | 9, 35 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Rel 𝐹) |
37 | | reltrclfv 14379 |
. . . . . . . 8
⊢ ((𝐹 ∈ V ∧ Rel 𝐹) → Rel (t+‘𝐹)) |
38 | 2, 36, 37 | syl2anc 586 |
. . . . . . 7
⊢ (𝜑 → Rel (t+‘𝐹)) |
39 | | brrelex1 5607 |
. . . . . . 7
⊢ ((Rel
(t+‘𝐹) ∧ 𝐵(t+‘𝐹)𝐴) → 𝐵 ∈ V) |
40 | 38, 39 | sylan 582 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐵 ∈ V) |
41 | | fvex 6685 |
. . . . . . . 8
⊢ (𝐹‘𝐴) ∈ V |
42 | 6, 41 | eqeltrdi 2923 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ V) |
43 | 42 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐶 ∈ V) |
44 | 4 | elexd 3516 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ V) |
45 | 44 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐴 ∈ V) |
46 | | simpr 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐵(t+‘𝐹)𝐴) |
47 | 27 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐴𝐹𝐶) |
48 | 34, 40, 43, 45, 46, 47 | frege96d 40101 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵(t+‘𝐹)𝐴) → 𝐵(t+‘𝐹)𝐶) |
49 | 48 | ex 415 |
. . . 4
⊢ (𝜑 → (𝐵(t+‘𝐹)𝐴 → 𝐵(t+‘𝐹)𝐶)) |
50 | 49, 32 | syl6 35 |
. . 3
⊢ (𝜑 → (𝐵(t+‘𝐹)𝐴 → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵))) |
51 | 21, 33, 50 | 3jaod 1424 |
. 2
⊢ (𝜑 → ((𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐴) → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵))) |
52 | 1, 51 | mpd 15 |
1
⊢ (𝜑 → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵)) |