Proof of Theorem oev2
Step | Hyp | Ref
| Expression |
1 | | oveq12 7179 |
. . . . . 6
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 ↑o 𝐵) = (∅ ↑o
∅)) |
2 | | oe0m0 8176 |
. . . . . 6
⊢ (∅
↑o ∅) = 1o |
3 | 1, 2 | eqtrdi 2789 |
. . . . 5
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 ↑o 𝐵) =
1o) |
4 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝐵 = ∅ → (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)),
1o)‘∅)) |
5 | | 1oex 8144 |
. . . . . . . . 9
⊢
1o ∈ V |
6 | 5 | rdg0 8086 |
. . . . . . . 8
⊢
(rec((𝑥 ∈ V
↦ (𝑥
·o 𝐴)),
1o)‘∅) = 1o |
7 | 4, 6 | eqtrdi 2789 |
. . . . . . 7
⊢ (𝐵 = ∅ → (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) =
1o) |
8 | | inteq 4839 |
. . . . . . . 8
⊢ (𝐵 = ∅ → ∩ 𝐵 =
∩ ∅) |
9 | | int0 4850 |
. . . . . . . 8
⊢ ∩ ∅ = V |
10 | 8, 9 | eqtrdi 2789 |
. . . . . . 7
⊢ (𝐵 = ∅ → ∩ 𝐵 =
V) |
11 | 7, 10 | ineq12d 4104 |
. . . . . 6
⊢ (𝐵 = ∅ → ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ∩ 𝐵) =
(1o ∩ V)) |
12 | | inv1 4283 |
. . . . . . 7
⊢
(1o ∩ V) = 1o |
13 | 12 | a1i 11 |
. . . . . 6
⊢ (𝐴 = ∅ → (1o
∩ V) = 1o) |
14 | 11, 13 | sylan9eqr 2795 |
. . . . 5
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ∩ 𝐵) =
1o) |
15 | 3, 14 | eqtr4d 2776 |
. . . 4
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 ↑o 𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ∩ 𝐵)) |
16 | | oveq1 7177 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝐴 ↑o 𝐵) = (∅ ↑o
𝐵)) |
17 | | oe0m1 8177 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑o 𝐵) =
∅)) |
18 | 17 | biimpa 480 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ ∅ ∈
𝐵) → (∅
↑o 𝐵) =
∅) |
19 | 16, 18 | sylan9eqr 2795 |
. . . . . 6
⊢ (((𝐵 ∈ On ∧ ∅ ∈
𝐵) ∧ 𝐴 = ∅) → (𝐴 ↑o 𝐵) = ∅) |
20 | 19 | an32s 652 |
. . . . 5
⊢ (((𝐵 ∈ On ∧ 𝐴 = ∅) ∧ ∅ ∈
𝐵) → (𝐴 ↑o 𝐵) = ∅) |
21 | | int0el 4867 |
. . . . . . . 8
⊢ (∅
∈ 𝐵 → ∩ 𝐵 =
∅) |
22 | 21 | ineq2d 4103 |
. . . . . . 7
⊢ (∅
∈ 𝐵 →
((rec((𝑥 ∈ V ↦
(𝑥 ·o
𝐴)),
1o)‘𝐵)
∩ ∩ 𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ∅)) |
23 | | in0 4280 |
. . . . . . 7
⊢
((rec((𝑥 ∈ V
↦ (𝑥
·o 𝐴)),
1o)‘𝐵)
∩ ∅) = ∅ |
24 | 22, 23 | eqtrdi 2789 |
. . . . . 6
⊢ (∅
∈ 𝐵 →
((rec((𝑥 ∈ V ↦
(𝑥 ·o
𝐴)),
1o)‘𝐵)
∩ ∩ 𝐵) = ∅) |
25 | 24 | adantl 485 |
. . . . 5
⊢ (((𝐵 ∈ On ∧ 𝐴 = ∅) ∧ ∅ ∈
𝐵) → ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ∩ 𝐵) =
∅) |
26 | 20, 25 | eqtr4d 2776 |
. . . 4
⊢ (((𝐵 ∈ On ∧ 𝐴 = ∅) ∧ ∅ ∈
𝐵) → (𝐴 ↑o 𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ∩ 𝐵)) |
27 | 15, 26 | oe0lem 8169 |
. . 3
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴 ↑o 𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ∩ 𝐵)) |
28 | | inteq 4839 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → ∩ 𝐴 =
∩ ∅) |
29 | 28, 9 | eqtrdi 2789 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → ∩ 𝐴 =
V) |
30 | 29 | difeq2d 4013 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (V ∖
∩ 𝐴) = (V ∖ V)) |
31 | | difid 4259 |
. . . . . . . 8
⊢ (V
∖ V) = ∅ |
32 | 30, 31 | eqtrdi 2789 |
. . . . . . 7
⊢ (𝐴 = ∅ → (V ∖
∩ 𝐴) = ∅) |
33 | 32 | uneq2d 4053 |
. . . . . 6
⊢ (𝐴 = ∅ → (∩ 𝐵
∪ (V ∖ ∩ 𝐴)) = (∩ 𝐵 ∪
∅)) |
34 | | uncom 4043 |
. . . . . 6
⊢ (∩ 𝐵
∪ (V ∖ ∩ 𝐴)) = ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵) |
35 | | un0 4279 |
. . . . . 6
⊢ (∩ 𝐵
∪ ∅) = ∩ 𝐵 |
36 | 33, 34, 35 | 3eqtr3g 2796 |
. . . . 5
⊢ (𝐴 = ∅ → ((V ∖
∩ 𝐴) ∪ ∩ 𝐵) = ∩
𝐵) |
37 | 36 | adantl 485 |
. . . 4
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → ((V ∖
∩ 𝐴) ∪ ∩ 𝐵) = ∩
𝐵) |
38 | 37 | ineq2d 4103 |
. . 3
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵)) = ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ∩ 𝐵)) |
39 | 27, 38 | eqtr4d 2776 |
. 2
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴 ↑o 𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵))) |
40 | | oevn0 8171 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝐴 ↑o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)) |
41 | | int0el 4867 |
. . . . . . . . . 10
⊢ (∅
∈ 𝐴 → ∩ 𝐴 =
∅) |
42 | 41 | difeq2d 4013 |
. . . . . . . . 9
⊢ (∅
∈ 𝐴 → (V ∖
∩ 𝐴) = (V ∖ ∅)) |
43 | | dif0 4261 |
. . . . . . . . 9
⊢ (V
∖ ∅) = V |
44 | 42, 43 | eqtrdi 2789 |
. . . . . . . 8
⊢ (∅
∈ 𝐴 → (V ∖
∩ 𝐴) = V) |
45 | 44 | uneq2d 4053 |
. . . . . . 7
⊢ (∅
∈ 𝐴 → (∩ 𝐵
∪ (V ∖ ∩ 𝐴)) = (∩ 𝐵 ∪ V)) |
46 | | unv 4284 |
. . . . . . 7
⊢ (∩ 𝐵
∪ V) = V |
47 | 45, 34, 46 | 3eqtr3g 2796 |
. . . . . 6
⊢ (∅
∈ 𝐴 → ((V ∖
∩ 𝐴) ∪ ∩ 𝐵) = V) |
48 | 47 | adantl 485 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵) = V) |
49 | 48 | ineq2d 4103 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵)) = ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ V)) |
50 | | inv1 4283 |
. . . 4
⊢
((rec((𝑥 ∈ V
↦ (𝑥
·o 𝐴)),
1o)‘𝐵)
∩ V) = (rec((𝑥 ∈ V
↦ (𝑥
·o 𝐴)),
1o)‘𝐵) |
51 | 49, 50 | eqtr2di 2790 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵))) |
52 | 40, 51 | eqtrd 2773 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝐴 ↑o 𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵))) |
53 | 39, 52 | oe0lem 8169 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵))) |