Proof of Theorem oev2
Step | Hyp | Ref
| Expression |
1 | | oveq12 6659 |
. . . . . 6
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 ↑𝑜
𝐵) = (∅
↑𝑜 ∅)) |
2 | | oe0m0 7600 |
. . . . . 6
⊢ (∅
↑𝑜 ∅) = 1𝑜 |
3 | 1, 2 | syl6eq 2672 |
. . . . 5
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 ↑𝑜
𝐵) =
1𝑜) |
4 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝐵 = ∅ → (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)),
1𝑜)‘∅)) |
5 | | 1on 7567 |
. . . . . . . . . 10
⊢
1𝑜 ∈ On |
6 | 5 | elexi 3213 |
. . . . . . . . 9
⊢
1𝑜 ∈ V |
7 | 6 | rdg0 7517 |
. . . . . . . 8
⊢
(rec((𝑥 ∈ V
↦ (𝑥
·𝑜 𝐴)), 1𝑜)‘∅) =
1𝑜 |
8 | 4, 7 | syl6eq 2672 |
. . . . . . 7
⊢ (𝐵 = ∅ → (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) = 1𝑜) |
9 | | inteq 4478 |
. . . . . . . 8
⊢ (𝐵 = ∅ → ∩ 𝐵 =
∩ ∅) |
10 | | int0 4490 |
. . . . . . . 8
⊢ ∩ ∅ = V |
11 | 9, 10 | syl6eq 2672 |
. . . . . . 7
⊢ (𝐵 = ∅ → ∩ 𝐵 =
V) |
12 | 8, 11 | ineq12d 3815 |
. . . . . 6
⊢ (𝐵 = ∅ → ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) ∩ ∩ 𝐵) = (1𝑜 ∩
V)) |
13 | | inv1 3970 |
. . . . . . 7
⊢
(1𝑜 ∩ V) = 1𝑜 |
14 | 13 | a1i 11 |
. . . . . 6
⊢ (𝐴 = ∅ →
(1𝑜 ∩ V) = 1𝑜) |
15 | 12, 14 | sylan9eqr 2678 |
. . . . 5
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) ∩ ∩ 𝐵) =
1𝑜) |
16 | 3, 15 | eqtr4d 2659 |
. . . 4
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 ↑𝑜
𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) ∩ ∩ 𝐵)) |
17 | | oveq1 6657 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝐴 ↑𝑜
𝐵) = (∅
↑𝑜 𝐵)) |
18 | | oe0m1 7601 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑𝑜 𝐵) = ∅)) |
19 | 18 | biimpa 501 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ ∅ ∈
𝐵) → (∅
↑𝑜 𝐵) = ∅) |
20 | 17, 19 | sylan9eqr 2678 |
. . . . . 6
⊢ (((𝐵 ∈ On ∧ ∅ ∈
𝐵) ∧ 𝐴 = ∅) → (𝐴 ↑𝑜 𝐵) = ∅) |
21 | 20 | an32s 846 |
. . . . 5
⊢ (((𝐵 ∈ On ∧ 𝐴 = ∅) ∧ ∅ ∈
𝐵) → (𝐴 ↑𝑜
𝐵) =
∅) |
22 | | int0el 4508 |
. . . . . . . 8
⊢ (∅
∈ 𝐵 → ∩ 𝐵 =
∅) |
23 | 22 | ineq2d 3814 |
. . . . . . 7
⊢ (∅
∈ 𝐵 →
((rec((𝑥 ∈ V ↦
(𝑥
·𝑜 𝐴)), 1𝑜)‘𝐵) ∩ ∩ 𝐵) =
((rec((𝑥 ∈ V ↦
(𝑥
·𝑜 𝐴)), 1𝑜)‘𝐵) ∩
∅)) |
24 | | in0 3968 |
. . . . . . 7
⊢
((rec((𝑥 ∈ V
↦ (𝑥
·𝑜 𝐴)), 1𝑜)‘𝐵) ∩ ∅) =
∅ |
25 | 23, 24 | syl6eq 2672 |
. . . . . 6
⊢ (∅
∈ 𝐵 →
((rec((𝑥 ∈ V ↦
(𝑥
·𝑜 𝐴)), 1𝑜)‘𝐵) ∩ ∩ 𝐵) =
∅) |
26 | 25 | adantl 482 |
. . . . 5
⊢ (((𝐵 ∈ On ∧ 𝐴 = ∅) ∧ ∅ ∈
𝐵) → ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) ∩ ∩ 𝐵) = ∅) |
27 | 21, 26 | eqtr4d 2659 |
. . . 4
⊢ (((𝐵 ∈ On ∧ 𝐴 = ∅) ∧ ∅ ∈
𝐵) → (𝐴 ↑𝑜
𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) ∩ ∩ 𝐵)) |
28 | 16, 27 | oe0lem 7593 |
. . 3
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴 ↑𝑜
𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) ∩ ∩ 𝐵)) |
29 | | inteq 4478 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → ∩ 𝐴 =
∩ ∅) |
30 | 29, 10 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → ∩ 𝐴 =
V) |
31 | 30 | difeq2d 3728 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (V ∖
∩ 𝐴) = (V ∖ V)) |
32 | | difid 3948 |
. . . . . . . 8
⊢ (V
∖ V) = ∅ |
33 | 31, 32 | syl6eq 2672 |
. . . . . . 7
⊢ (𝐴 = ∅ → (V ∖
∩ 𝐴) = ∅) |
34 | 33 | uneq2d 3767 |
. . . . . 6
⊢ (𝐴 = ∅ → (∩ 𝐵
∪ (V ∖ ∩ 𝐴)) = (∩ 𝐵 ∪
∅)) |
35 | | uncom 3757 |
. . . . . 6
⊢ (∩ 𝐵
∪ (V ∖ ∩ 𝐴)) = ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵) |
36 | | un0 3967 |
. . . . . 6
⊢ (∩ 𝐵
∪ ∅) = ∩ 𝐵 |
37 | 34, 35, 36 | 3eqtr3g 2679 |
. . . . 5
⊢ (𝐴 = ∅ → ((V ∖
∩ 𝐴) ∪ ∩ 𝐵) = ∩
𝐵) |
38 | 37 | adantl 482 |
. . . 4
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → ((V ∖
∩ 𝐴) ∪ ∩ 𝐵) = ∩
𝐵) |
39 | 38 | ineq2d 3814 |
. . 3
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) ∩ ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵)) = ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)),
1𝑜)‘𝐵) ∩ ∩ 𝐵)) |
40 | 28, 39 | eqtr4d 2659 |
. 2
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴 ↑𝑜
𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) ∩ ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵))) |
41 | | oevn0 7595 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝐴 ↑𝑜
𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵)) |
42 | | int0el 4508 |
. . . . . . . . . 10
⊢ (∅
∈ 𝐴 → ∩ 𝐴 =
∅) |
43 | 42 | difeq2d 3728 |
. . . . . . . . 9
⊢ (∅
∈ 𝐴 → (V ∖
∩ 𝐴) = (V ∖ ∅)) |
44 | | dif0 3950 |
. . . . . . . . 9
⊢ (V
∖ ∅) = V |
45 | 43, 44 | syl6eq 2672 |
. . . . . . . 8
⊢ (∅
∈ 𝐴 → (V ∖
∩ 𝐴) = V) |
46 | 45 | uneq2d 3767 |
. . . . . . 7
⊢ (∅
∈ 𝐴 → (∩ 𝐵
∪ (V ∖ ∩ 𝐴)) = (∩ 𝐵 ∪ V)) |
47 | | unv 3971 |
. . . . . . 7
⊢ (∩ 𝐵
∪ V) = V |
48 | 46, 35, 47 | 3eqtr3g 2679 |
. . . . . 6
⊢ (∅
∈ 𝐴 → ((V ∖
∩ 𝐴) ∪ ∩ 𝐵) = V) |
49 | 48 | adantl 482 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵) = V) |
50 | 49 | ineq2d 3814 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) ∩ ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵)) = ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)),
1𝑜)‘𝐵) ∩ V)) |
51 | | inv1 3970 |
. . . 4
⊢
((rec((𝑥 ∈ V
↦ (𝑥
·𝑜 𝐴)), 1𝑜)‘𝐵) ∩ V) = (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) |
52 | 50, 51 | syl6req 2673 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)),
1𝑜)‘𝐵) ∩ ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵))) |
53 | 41, 52 | eqtrd 2656 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝐴 ↑𝑜
𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) ∩ ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵))) |
54 | 40, 53 | oe0lem 7593 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜
𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵) ∩ ((V ∖ ∩ 𝐴)
∪ ∩ 𝐵))) |