Step | Hyp | Ref
| Expression |
1 | | oveq12 7370 |
. . . . . 6
โข ((๐ด = โ
โง ๐ต = โ
) โ (๐ด โo ๐ต) = (โ
โo
โ
)) |
2 | | oe0m0 8470 |
. . . . . 6
โข (โ
โo โ
) = 1o |
3 | 1, 2 | eqtrdi 2789 |
. . . . 5
โข ((๐ด = โ
โง ๐ต = โ
) โ (๐ด โo ๐ต) =
1o) |
4 | | fveq2 6846 |
. . . . . . . 8
โข (๐ต = โ
โ (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต) = (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)),
1o)โโ
)) |
5 | | 1oex 8426 |
. . . . . . . . 9
โข
1o โ V |
6 | 5 | rdg0 8371 |
. . . . . . . 8
โข
(rec((๐ฅ โ V
โฆ (๐ฅ
ยทo ๐ด)),
1o)โโ
) = 1o |
7 | 4, 6 | eqtrdi 2789 |
. . . . . . 7
โข (๐ต = โ
โ (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต) =
1o) |
8 | | inteq 4914 |
. . . . . . . 8
โข (๐ต = โ
โ โฉ ๐ต =
โฉ โ
) |
9 | | int0 4927 |
. . . . . . . 8
โข โฉ โ
= V |
10 | 8, 9 | eqtrdi 2789 |
. . . . . . 7
โข (๐ต = โ
โ โฉ ๐ต =
V) |
11 | 7, 10 | ineq12d 4177 |
. . . . . 6
โข (๐ต = โ
โ ((rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต) โฉ โฉ ๐ต) =
(1o โฉ V)) |
12 | | inv1 4358 |
. . . . . . 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 7368 |
. . . . . . 7
โข (๐ด = โ
โ (๐ด โo ๐ต) = (โ
โo
๐ต)) |
17 | | oe0m1 8471 |
. . . . . . . 8
โข (๐ต โ On โ (โ
โ ๐ต โ (โ
โo ๐ต) =
โ
)) |
18 | 17 | biimpa 478 |
. . . . . . 7
โข ((๐ต โ On โง โ
โ
๐ต) โ (โ
โo ๐ต) =
โ
) |
19 | 16, 18 | sylan9eqr 2795 |
. . . . . 6
โข (((๐ต โ On โง โ
โ
๐ต) โง ๐ด = โ
) โ (๐ด โo ๐ต) = โ
) |
20 | 19 | an32s 651 |
. . . . 5
โข (((๐ต โ On โง ๐ด = โ
) โง โ
โ
๐ต) โ (๐ด โo ๐ต) = โ
) |
21 | | int0el 4944 |
. . . . . . . 8
โข (โ
โ ๐ต โ โฉ ๐ต =
โ
) |
22 | 21 | ineq2d 4176 |
. . . . . . 7
โข (โ
โ ๐ต โ
((rec((๐ฅ โ V โฆ
(๐ฅ ยทo
๐ด)),
1o)โ๐ต)
โฉ โฉ ๐ต) = ((rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต) โฉ โ
)) |
23 | | in0 4355 |
. . . . . . 7
โข
((rec((๐ฅ โ V
โฆ (๐ฅ
ยทo ๐ด)),
1o)โ๐ต)
โฉ โ
) = โ
|
24 | 22, 23 | eqtrdi 2789 |
. . . . . 6
โข (โ
โ ๐ต โ
((rec((๐ฅ โ V โฆ
(๐ฅ ยทo
๐ด)),
1o)โ๐ต)
โฉ โฉ ๐ต) = โ
) |
25 | 24 | adantl 483 |
. . . . 5
โข (((๐ต โ On โง ๐ด = โ
) โง โ
โ
๐ต) โ ((rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต) โฉ โฉ ๐ต) =
โ
) |
26 | 20, 25 | eqtr4d 2776 |
. . . 4
โข (((๐ต โ On โง ๐ด = โ
) โง โ
โ
๐ต) โ (๐ด โo ๐ต) = ((rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต) โฉ โฉ ๐ต)) |
27 | 15, 26 | oe0lem 8463 |
. . 3
โข ((๐ต โ On โง ๐ด = โ
) โ (๐ด โo ๐ต) = ((rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต) โฉ โฉ ๐ต)) |
28 | | inteq 4914 |
. . . . . . . . . 10
โข (๐ด = โ
โ โฉ ๐ด =
โฉ โ
) |
29 | 28, 9 | eqtrdi 2789 |
. . . . . . . . 9
โข (๐ด = โ
โ โฉ ๐ด =
V) |
30 | 29 | difeq2d 4086 |
. . . . . . . 8
โข (๐ด = โ
โ (V โ
โฉ ๐ด) = (V โ V)) |
31 | | difid 4334 |
. . . . . . . 8
โข (V
โ V) = โ
|
32 | 30, 31 | eqtrdi 2789 |
. . . . . . 7
โข (๐ด = โ
โ (V โ
โฉ ๐ด) = โ
) |
33 | 32 | uneq2d 4127 |
. . . . . 6
โข (๐ด = โ
โ (โฉ ๐ต
โช (V โ โฉ ๐ด)) = (โฉ ๐ต โช
โ
)) |
34 | | uncom 4117 |
. . . . . 6
โข (โฉ ๐ต
โช (V โ โฉ ๐ด)) = ((V โ โฉ ๐ด)
โช โฉ ๐ต) |
35 | | un0 4354 |
. . . . . 6
โข (โฉ ๐ต
โช โ
) = โฉ ๐ต |
36 | 33, 34, 35 | 3eqtr3g 2796 |
. . . . 5
โข (๐ด = โ
โ ((V โ
โฉ ๐ด) โช โฉ ๐ต) = โฉ
๐ต) |
37 | 36 | adantl 483 |
. . . 4
โข ((๐ต โ On โง ๐ด = โ
) โ ((V โ
โฉ ๐ด) โช โฉ ๐ต) = โฉ
๐ต) |
38 | 37 | ineq2d 4176 |
. . 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 8465 |
. . 3
โข (((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ด) โ (๐ด โo ๐ต) = (rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต)) |
41 | | int0el 4944 |
. . . . . . . . . 10
โข (โ
โ ๐ด โ โฉ ๐ด =
โ
) |
42 | 41 | difeq2d 4086 |
. . . . . . . . 9
โข (โ
โ ๐ด โ (V โ
โฉ ๐ด) = (V โ โ
)) |
43 | | dif0 4336 |
. . . . . . . . 9
โข (V
โ โ
) = V |
44 | 42, 43 | eqtrdi 2789 |
. . . . . . . 8
โข (โ
โ ๐ด โ (V โ
โฉ ๐ด) = V) |
45 | 44 | uneq2d 4127 |
. . . . . . 7
โข (โ
โ ๐ด โ (โฉ ๐ต
โช (V โ โฉ ๐ด)) = (โฉ ๐ต โช V)) |
46 | | unv 4359 |
. . . . . . 7
โข (โฉ ๐ต
โช V) = V |
47 | 45, 34, 46 | 3eqtr3g 2796 |
. . . . . 6
โข (โ
โ ๐ด โ ((V โ
โฉ ๐ด) โช โฉ ๐ต) = V) |
48 | 47 | adantl 483 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ด) โ ((V โ โฉ ๐ด)
โช โฉ ๐ต) = V) |
49 | 48 | ineq2d 4176 |
. . . 4
โข (((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ด) โ ((rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต) โฉ ((V โ โฉ ๐ด)
โช โฉ ๐ต)) = ((rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต) โฉ V)) |
50 | | inv1 4358 |
. . . 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 8463 |
1
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โo ๐ต) = ((rec((๐ฅ โ V โฆ (๐ฅ ยทo ๐ด)), 1o)โ๐ต) โฉ ((V โ โฉ ๐ด)
โช โฉ ๐ต))) |