Proof of Theorem sbcoteq1a
Step | Hyp | Ref
| Expression |
1 | | fveq2 6891 |
. . . 4
⊢ (𝐴 = 〈𝑥, 𝑦, 𝑧〉 → (2nd ‘𝐴) = (2nd
‘〈𝑥, 𝑦, 𝑧〉)) |
2 | | ot3rdg 8003 |
. . . . 5
⊢ (𝑧 ∈ V → (2nd
‘〈𝑥, 𝑦, 𝑧〉) = 𝑧) |
3 | 2 | elv 3475 |
. . . 4
⊢
(2nd ‘〈𝑥, 𝑦, 𝑧〉) = 𝑧 |
4 | 1, 3 | eqtr2di 2784 |
. . 3
⊢ (𝐴 = 〈𝑥, 𝑦, 𝑧〉 → 𝑧 = (2nd ‘𝐴)) |
5 | | sbceq1a 3785 |
. . 3
⊢ (𝑧 = (2nd ‘𝐴) → (𝜑 ↔ [(2nd ‘𝐴) / 𝑧]𝜑)) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝐴 = 〈𝑥, 𝑦, 𝑧〉 → (𝜑 ↔ [(2nd ‘𝐴) / 𝑧]𝜑)) |
7 | | 2fveq3 6896 |
. . . 4
⊢ (𝐴 = 〈𝑥, 𝑦, 𝑧〉 → (2nd
‘(1st ‘𝐴)) = (2nd ‘(1st
‘〈𝑥, 𝑦, 𝑧〉))) |
8 | | vex 3473 |
. . . . 5
⊢ 𝑥 ∈ V |
9 | | vex 3473 |
. . . . 5
⊢ 𝑦 ∈ V |
10 | | vex 3473 |
. . . . 5
⊢ 𝑧 ∈ V |
11 | | ot2ndg 8002 |
. . . . 5
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) →
(2nd ‘(1st ‘〈𝑥, 𝑦, 𝑧〉)) = 𝑦) |
12 | 8, 9, 10, 11 | mp3an 1458 |
. . . 4
⊢
(2nd ‘(1st ‘〈𝑥, 𝑦, 𝑧〉)) = 𝑦 |
13 | 7, 12 | eqtr2di 2784 |
. . 3
⊢ (𝐴 = 〈𝑥, 𝑦, 𝑧〉 → 𝑦 = (2nd ‘(1st
‘𝐴))) |
14 | | sbceq1a 3785 |
. . 3
⊢ (𝑦 = (2nd
‘(1st ‘𝐴)) → ([(2nd
‘𝐴) / 𝑧]𝜑 ↔ [(2nd
‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑)) |
15 | 13, 14 | syl 17 |
. 2
⊢ (𝐴 = 〈𝑥, 𝑦, 𝑧〉 → ([(2nd
‘𝐴) / 𝑧]𝜑 ↔ [(2nd
‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑)) |
16 | | 2fveq3 6896 |
. . . 4
⊢ (𝐴 = 〈𝑥, 𝑦, 𝑧〉 → (1st
‘(1st ‘𝐴)) = (1st ‘(1st
‘〈𝑥, 𝑦, 𝑧〉))) |
17 | | ot1stg 8001 |
. . . . 5
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) →
(1st ‘(1st ‘〈𝑥, 𝑦, 𝑧〉)) = 𝑥) |
18 | 8, 9, 10, 17 | mp3an 1458 |
. . . 4
⊢
(1st ‘(1st ‘〈𝑥, 𝑦, 𝑧〉)) = 𝑥 |
19 | 16, 18 | eqtr2di 2784 |
. . 3
⊢ (𝐴 = 〈𝑥, 𝑦, 𝑧〉 → 𝑥 = (1st ‘(1st
‘𝐴))) |
20 | | sbceq1a 3785 |
. . 3
⊢ (𝑥 = (1st
‘(1st ‘𝐴)) → ([(2nd
‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑 ↔ [(1st
‘(1st ‘𝐴)) / 𝑥][(2nd
‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑)) |
21 | 19, 20 | syl 17 |
. 2
⊢ (𝐴 = 〈𝑥, 𝑦, 𝑧〉 → ([(2nd
‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑 ↔ [(1st
‘(1st ‘𝐴)) / 𝑥][(2nd
‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑)) |
22 | 6, 15, 21 | 3bitrrd 306 |
1
⊢ (𝐴 = 〈𝑥, 𝑦, 𝑧〉 → ([(1st
‘(1st ‘𝐴)) / 𝑥][(2nd
‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑 ↔ 𝜑)) |