Proof of Theorem 2arymptfv
Step | Hyp | Ref
| Expression |
1 | | 2arympt.f |
. 2
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑥‘0)𝑂(𝑥‘1))) |
2 | | fveq1 6650 |
. . . . 5
⊢ (𝑥 = {〈0, 𝐴〉, 〈1, 𝐵〉} → (𝑥‘0) = ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0)) |
3 | 2 | adantl 486 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 = {〈0, 𝐴〉, 〈1, 𝐵〉}) → (𝑥‘0) = ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0)) |
4 | | c0ex 10658 |
. . . . . . . 8
⊢ 0 ∈
V |
5 | 4 | a1i 11 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ∈ V) |
6 | | simp2 1135 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐴 ∈ 𝑋) |
7 | | 0ne1 11730 |
. . . . . . . 8
⊢ 0 ≠
1 |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≠ 1) |
9 | 5, 6, 8 | 3jca 1126 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (0 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 0 ≠ 1)) |
10 | 9 | adantr 485 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 = {〈0, 𝐴〉, 〈1, 𝐵〉}) → (0 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 0 ≠ 1)) |
11 | | fvpr1g 6938 |
. . . . 5
⊢ ((0
∈ V ∧ 𝐴 ∈
𝑋 ∧ 0 ≠ 1) →
({〈0, 𝐴〉,
〈1, 𝐵〉}‘0)
= 𝐴) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 = {〈0, 𝐴〉, 〈1, 𝐵〉}) → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0) = 𝐴) |
13 | 3, 12 | eqtrd 2794 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 = {〈0, 𝐴〉, 〈1, 𝐵〉}) → (𝑥‘0) = 𝐴) |
14 | | fveq1 6650 |
. . . 4
⊢ (𝑥 = {〈0, 𝐴〉, 〈1, 𝐵〉} → (𝑥‘1) = ({〈0, 𝐴〉, 〈1, 𝐵〉}‘1)) |
15 | | 1ex 10660 |
. . . . 5
⊢ 1 ∈
V |
16 | | simp3 1136 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋) |
17 | | fvpr2g 6939 |
. . . . 5
⊢ ((1
∈ V ∧ 𝐵 ∈
𝑋 ∧ 0 ≠ 1) →
({〈0, 𝐴〉,
〈1, 𝐵〉}‘1)
= 𝐵) |
18 | 15, 16, 8, 17 | mp3an2i 1464 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘1) = 𝐵) |
19 | 14, 18 | sylan9eqr 2816 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 = {〈0, 𝐴〉, 〈1, 𝐵〉}) → (𝑥‘1) = 𝐵) |
20 | 13, 19 | oveq12d 7161 |
. 2
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 = {〈0, 𝐴〉, 〈1, 𝐵〉}) → ((𝑥‘0)𝑂(𝑥‘1)) = (𝐴𝑂𝐵)) |
21 | | simp1 1134 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝑋 ∈ 𝑉) |
22 | 4, 15, 7 | 3pm3.2i 1337 |
. . . 4
⊢ (0 ∈
V ∧ 1 ∈ V ∧ 0 ≠ 1) |
23 | 22 | a1i 11 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (0 ∈ V ∧ 1 ∈ V ∧
0 ≠ 1)) |
24 | | 3simpc 1148 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) |
25 | | fprmappr 45099 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ (0 ∈ V ∧ 1 ∈ V ∧ 0
≠ 1) ∧ (𝐴 ∈
𝑋 ∧ 𝐵 ∈ 𝑋)) → {〈0, 𝐴〉, 〈1, 𝐵〉} ∈ (𝑋 ↑m {0,
1})) |
26 | 21, 23, 24, 25 | syl3anc 1369 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {〈0, 𝐴〉, 〈1, 𝐵〉} ∈ (𝑋 ↑m {0,
1})) |
27 | | ovexd 7178 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑂𝐵) ∈ V) |
28 | 1, 20, 26, 27 | fvmptd2 6760 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘{〈0, 𝐴〉, 〈1, 𝐵〉}) = (𝐴𝑂𝐵)) |