Step | Hyp | Ref
| Expression |
1 | | 2arympt.f |
. 2
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑥‘0)𝑂(𝑥‘1))) |
2 | | fveq1 6889 |
. . . . 5
⊢ (𝑥 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩} → (𝑥‘0) = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩}‘0)) |
3 | 2 | adantl 480 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩}) → (𝑥‘0) = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩}‘0)) |
4 | | c0ex 11212 |
. . . . . . . 8
⊢ 0 ∈
V |
5 | 4 | a1i 11 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ∈ V) |
6 | | simp2 1135 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐴 ∈ 𝑋) |
7 | | 0ne1 12287 |
. . . . . . . 8
⊢ 0 ≠
1 |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≠ 1) |
9 | 5, 6, 8 | 3jca 1126 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (0 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 0 ≠ 1)) |
10 | 9 | adantr 479 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩}) → (0 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 0 ≠ 1)) |
11 | | fvpr1g 7189 |
. . . . 5
⊢ ((0
∈ V ∧ 𝐴 ∈
𝑋 ∧ 0 ≠ 1) →
({⟨0, 𝐴⟩,
⟨1, 𝐵⟩}‘0)
= 𝐴) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩}) → ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩}‘0) = 𝐴) |
13 | 3, 12 | eqtrd 2770 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩}) → (𝑥‘0) = 𝐴) |
14 | | fveq1 6889 |
. . . 4
⊢ (𝑥 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩} → (𝑥‘1) = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩}‘1)) |
15 | | 1ex 11214 |
. . . . 5
⊢ 1 ∈
V |
16 | | simp3 1136 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋) |
17 | | fvpr2g 7190 |
. . . . 5
⊢ ((1
∈ V ∧ 𝐵 ∈
𝑋 ∧ 0 ≠ 1) →
({⟨0, 𝐴⟩,
⟨1, 𝐵⟩}‘1)
= 𝐵) |
18 | 15, 16, 8, 17 | mp3an2i 1464 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩}‘1) = 𝐵) |
19 | 14, 18 | sylan9eqr 2792 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩}) → (𝑥‘1) = 𝐵) |
20 | 13, 19 | oveq12d 7429 |
. 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 47109 |
. . 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 7446 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑂𝐵) ∈ V) |
28 | 1, 20, 26, 27 | fvmptd2 7005 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘{⟨0, 𝐴⟩, ⟨1, 𝐵⟩}) = (𝐴𝑂𝐵)) |