Step | Hyp | Ref
| Expression |
1 | | hsmexlem4.o |
. . . . . . 7
β’ π = OrdIso( E , (rank β
((πβπ)βπ))) |
2 | | fveq2 6804 |
. . . . . . . . 9
β’ (π = β
β ((πβπ)βπ) = ((πβπ)ββ
)) |
3 | 2 | imaeq2d 5979 |
. . . . . . . 8
β’ (π = β
β (rank β
((πβπ)βπ)) = (rank β ((πβπ)ββ
))) |
4 | | oieq2 9320 |
. . . . . . . 8
β’ ((rank
β ((πβπ)βπ)) = (rank β ((πβπ)ββ
)) β OrdIso( E , (rank
β ((πβπ)βπ))) = OrdIso( E , (rank β ((πβπ)ββ
)))) |
5 | 3, 4 | syl 17 |
. . . . . . 7
β’ (π = β
β OrdIso( E ,
(rank β ((πβπ)βπ))) = OrdIso( E , (rank β ((πβπ)ββ
)))) |
6 | 1, 5 | eqtrid 2788 |
. . . . . 6
β’ (π = β
β π = OrdIso( E , (rank β
((πβπ)ββ
)))) |
7 | 6 | dmeqd 5827 |
. . . . 5
β’ (π = β
β dom π = dom OrdIso( E , (rank β
((πβπ)ββ
)))) |
8 | | fveq2 6804 |
. . . . 5
β’ (π = β
β (π»βπ) = (π»ββ
)) |
9 | 7, 8 | eleq12d 2831 |
. . . 4
β’ (π = β
β (dom π β (π»βπ) β dom OrdIso( E , (rank β
((πβπ)ββ
))) β (π»ββ
))) |
10 | 9 | ralbidv 3171 |
. . 3
β’ (π = β
β (βπ β π dom π β (π»βπ) β βπ β π dom OrdIso( E , (rank β ((πβπ)ββ
))) β (π»ββ
))) |
11 | | fveq2 6804 |
. . . . . . . . 9
β’ (π = π β ((πβπ)βπ) = ((πβπ)βπ)) |
12 | 11 | imaeq2d 5979 |
. . . . . . . 8
β’ (π = π β (rank β ((πβπ)βπ)) = (rank β ((πβπ)βπ))) |
13 | | oieq2 9320 |
. . . . . . . 8
β’ ((rank
β ((πβπ)βπ)) = (rank β ((πβπ)βπ)) β OrdIso( E , (rank β ((πβπ)βπ))) = OrdIso( E , (rank β ((πβπ)βπ)))) |
14 | 12, 13 | syl 17 |
. . . . . . 7
β’ (π = π β OrdIso( E , (rank β ((πβπ)βπ))) = OrdIso( E , (rank β ((πβπ)βπ)))) |
15 | 1, 14 | eqtrid 2788 |
. . . . . 6
β’ (π = π β π = OrdIso( E , (rank β ((πβπ)βπ)))) |
16 | 15 | dmeqd 5827 |
. . . . 5
β’ (π = π β dom π = dom OrdIso( E , (rank β ((πβπ)βπ)))) |
17 | | fveq2 6804 |
. . . . 5
β’ (π = π β (π»βπ) = (π»βπ)) |
18 | 16, 17 | eleq12d 2831 |
. . . 4
β’ (π = π β (dom π β (π»βπ) β dom OrdIso( E , (rank β
((πβπ)βπ))) β (π»βπ))) |
19 | 18 | ralbidv 3171 |
. . 3
β’ (π = π β (βπ β π dom π β (π»βπ) β βπ β π dom OrdIso( E , (rank β ((πβπ)βπ))) β (π»βπ))) |
20 | | fveq2 6804 |
. . . . . . . . 9
β’ (π = suc π β ((πβπ)βπ) = ((πβπ)βsuc π)) |
21 | 20 | imaeq2d 5979 |
. . . . . . . 8
β’ (π = suc π β (rank β ((πβπ)βπ)) = (rank β ((πβπ)βsuc π))) |
22 | | oieq2 9320 |
. . . . . . . 8
β’ ((rank
β ((πβπ)βπ)) = (rank β ((πβπ)βsuc π)) β OrdIso( E , (rank β ((πβπ)βπ))) = OrdIso( E , (rank β ((πβπ)βsuc π)))) |
23 | 21, 22 | syl 17 |
. . . . . . 7
β’ (π = suc π β OrdIso( E , (rank β ((πβπ)βπ))) = OrdIso( E , (rank β ((πβπ)βsuc π)))) |
24 | 1, 23 | eqtrid 2788 |
. . . . . 6
β’ (π = suc π β π = OrdIso( E , (rank β ((πβπ)βsuc π)))) |
25 | 24 | dmeqd 5827 |
. . . . 5
β’ (π = suc π β dom π = dom OrdIso( E , (rank β ((πβπ)βsuc π)))) |
26 | | fveq2 6804 |
. . . . 5
β’ (π = suc π β (π»βπ) = (π»βsuc π)) |
27 | 25, 26 | eleq12d 2831 |
. . . 4
β’ (π = suc π β (dom π β (π»βπ) β dom OrdIso( E , (rank β
((πβπ)βsuc π))) β (π»βsuc π))) |
28 | 27 | ralbidv 3171 |
. . 3
β’ (π = suc π β (βπ β π dom π β (π»βπ) β βπ β π dom OrdIso( E , (rank β ((πβπ)βsuc π))) β (π»βsuc π))) |
29 | | imassrn 5990 |
. . . . . . 7
β’ (rank
β ((πβπ)ββ
)) β ran
rank |
30 | | rankf 9600 |
. . . . . . . 8
β’
rank:βͺ (π
1 β
On)βΆOn |
31 | | frn 6637 |
. . . . . . . 8
β’
(rank:βͺ (π
1 β
On)βΆOn β ran rank β On) |
32 | 30, 31 | ax-mp 5 |
. . . . . . 7
β’ ran rank
β On |
33 | 29, 32 | sstri 3935 |
. . . . . 6
β’ (rank
β ((πβπ)ββ
)) β
On |
34 | | hsmexlem4.u |
. . . . . . . . . 10
β’ π = (π₯ β V β¦ (rec((π¦ β V β¦ βͺ π¦),
π₯) βΎ
Ο)) |
35 | 34 | ituni0 10224 |
. . . . . . . . 9
β’ (π β V β ((πβπ)ββ
) = π) |
36 | 35 | elv 3443 |
. . . . . . . 8
β’ ((πβπ)ββ
) = π |
37 | 36 | imaeq2i 5977 |
. . . . . . 7
β’ (rank
β ((πβπ)ββ
)) = (rank
β π) |
38 | | ffun 6633 |
. . . . . . . . . 10
β’
(rank:βͺ (π
1 β
On)βΆOn β Fun rank) |
39 | 30, 38 | ax-mp 5 |
. . . . . . . . 9
β’ Fun
rank |
40 | | vex 3441 |
. . . . . . . . 9
β’ π β V |
41 | | wdomimag 9394 |
. . . . . . . . 9
β’ ((Fun
rank β§ π β V)
β (rank β π)
βΌ* π) |
42 | 39, 40, 41 | mp2an 690 |
. . . . . . . 8
β’ (rank
β π)
βΌ* π |
43 | | sneq 4575 |
. . . . . . . . . . . . 13
β’ (π = π β {π} = {π}) |
44 | 43 | fveq2d 6808 |
. . . . . . . . . . . 12
β’ (π = π β (TCβ{π}) = (TCβ{π})) |
45 | 44 | raleqdv 3367 |
. . . . . . . . . . 11
β’ (π = π β (βπ β (TCβ{π})π βΌ π β βπ β (TCβ{π})π βΌ π)) |
46 | | hsmexlem4.s |
. . . . . . . . . . 11
β’ π = {π β βͺ
(π
1 β On) β£ βπ β (TCβ{π})π βΌ π} |
47 | 45, 46 | elrab2 3632 |
. . . . . . . . . 10
β’ (π β π β (π β βͺ
(π
1 β On) β§ βπ β (TCβ{π})π βΌ π)) |
48 | 47 | simprbi 498 |
. . . . . . . . 9
β’ (π β π β βπ β (TCβ{π})π βΌ π) |
49 | | snex 5363 |
. . . . . . . . . . . 12
β’ {π} β V |
50 | | tcid 9545 |
. . . . . . . . . . . 12
β’ ({π} β V β {π} β (TCβ{π})) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . 11
β’ {π} β (TCβ{π}) |
52 | | vsnid 4602 |
. . . . . . . . . . 11
β’ π β {π} |
53 | 51, 52 | sselii 3923 |
. . . . . . . . . 10
β’ π β (TCβ{π}) |
54 | | breq1 5084 |
. . . . . . . . . . 11
β’ (π = π β (π βΌ π β π βΌ π)) |
55 | 54 | rspcv 3562 |
. . . . . . . . . 10
β’ (π β (TCβ{π}) β (βπ β (TCβ{π})π βΌ π β π βΌ π)) |
56 | 53, 55 | ax-mp 5 |
. . . . . . . . 9
β’
(βπ β
(TCβ{π})π βΌ π β π βΌ π) |
57 | | domwdom 9381 |
. . . . . . . . 9
β’ (π βΌ π β π βΌ* π) |
58 | 48, 56, 57 | 3syl 18 |
. . . . . . . 8
β’ (π β π β π βΌ* π) |
59 | | wdomtr 9382 |
. . . . . . . 8
β’ (((rank
β π)
βΌ* π β§
π βΌ* π) β (rank β π) βΌ* π) |
60 | 42, 58, 59 | sylancr 588 |
. . . . . . 7
β’ (π β π β (rank β π) βΌ* π) |
61 | 37, 60 | eqbrtrid 5116 |
. . . . . 6
β’ (π β π β (rank β ((πβπ)ββ
)) βΌ* π) |
62 | | eqid 2736 |
. . . . . . 7
β’ OrdIso( E
, (rank β ((πβπ)ββ
))) = OrdIso( E , (rank
β ((πβπ)ββ
))) |
63 | 62 | hsmexlem1 10232 |
. . . . . 6
β’ (((rank
β ((πβπ)ββ
)) β On
β§ (rank β ((πβπ)ββ
)) βΌ* π) β dom OrdIso( E , (rank
β ((πβπ)ββ
))) β
(harβπ« π)) |
64 | 33, 61, 63 | sylancr 588 |
. . . . 5
β’ (π β π β dom OrdIso( E , (rank β
((πβπ)ββ
))) β
(harβπ« π)) |
65 | | hsmexlem4.h |
. . . . . 6
β’ π» = (rec((π§ β V β¦ (harβπ« (π Γ π§))), (harβπ« π)) βΎ Ο) |
66 | 65 | hsmexlem7 10229 |
. . . . 5
β’ (π»ββ
) =
(harβπ« π) |
67 | 64, 66 | eleqtrrdi 2848 |
. . . 4
β’ (π β π β dom OrdIso( E , (rank β
((πβπ)ββ
))) β (π»ββ
)) |
68 | 67 | rgen 3064 |
. . 3
β’
βπ β
π dom OrdIso( E , (rank
β ((πβπ)ββ
))) β (π»ββ
) |
69 | | nfra1 3264 |
. . . . . 6
β’
β²πβπ β π dom OrdIso( E , (rank β ((πβπ)βπ))) β (π»βπ) |
70 | | nfv 1915 |
. . . . . 6
β’
β²π π β Ο |
71 | 69, 70 | nfan 1900 |
. . . . 5
β’
β²π(βπ β π dom OrdIso( E , (rank β ((πβπ)βπ))) β (π»βπ) β§ π β Ο) |
72 | 34 | ituniiun 10228 |
. . . . . . . . . . . . 13
β’ (π β V β ((πβπ)βsuc π) = βͺ π β π ((πβπ)βπ)) |
73 | 72 | elv 3443 |
. . . . . . . . . . . 12
β’ ((πβπ)βsuc π) = βͺ π β π ((πβπ)βπ) |
74 | 73 | imaeq2i 5977 |
. . . . . . . . . . 11
β’ (rank
β ((πβπ)βsuc π)) = (rank β βͺ π β π ((πβπ)βπ)) |
75 | | imaiun 7150 |
. . . . . . . . . . 11
β’ (rank
β βͺ π β π ((πβπ)βπ)) = βͺ
π β π (rank β ((πβπ)βπ)) |
76 | 74, 75 | eqtri 2764 |
. . . . . . . . . 10
β’ (rank
β ((πβπ)βsuc π)) = βͺ
π β π (rank β ((πβπ)βπ)) |
77 | | oieq2 9320 |
. . . . . . . . . 10
β’ ((rank
β ((πβπ)βsuc π)) = βͺ
π β π (rank β ((πβπ)βπ)) β OrdIso( E , (rank β ((πβπ)βsuc π))) = OrdIso( E , βͺ π β π (rank β ((πβπ)βπ)))) |
78 | 76, 77 | ax-mp 5 |
. . . . . . . . 9
β’ OrdIso( E
, (rank β ((πβπ)βsuc π))) = OrdIso( E , βͺ π β π (rank β ((πβπ)βπ))) |
79 | 78 | dmeqi 5826 |
. . . . . . . 8
β’ dom
OrdIso( E , (rank β ((πβπ)βsuc π))) = dom OrdIso( E , βͺ π β π (rank β ((πβπ)βπ))) |
80 | 58 | ad2antll 727 |
. . . . . . . . 9
β’
((βπ β
π dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ) β§ (π β Ο β§ π β π)) β π βΌ* π) |
81 | 65 | hsmexlem9 10231 |
. . . . . . . . . 10
β’ (π β Ο β (π»βπ) β On) |
82 | 81 | ad2antrl 726 |
. . . . . . . . 9
β’
((βπ β
π dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ) β§ (π β Ο β§ π β π)) β (π»βπ) β On) |
83 | | fveq2 6804 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πβπ) = (πβπ)) |
84 | 83 | fveq1d 6806 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((πβπ)βπ) = ((πβπ)βπ)) |
85 | 84 | imaeq2d 5979 |
. . . . . . . . . . . . . . 15
β’ (π = π β (rank β ((πβπ)βπ)) = (rank β ((πβπ)βπ))) |
86 | | oieq2 9320 |
. . . . . . . . . . . . . . 15
β’ ((rank
β ((πβπ)βπ)) = (rank β ((πβπ)βπ)) β OrdIso( E , (rank β ((πβπ)βπ))) = OrdIso( E , (rank β ((πβπ)βπ)))) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π = π β OrdIso( E , (rank β ((πβπ)βπ))) = OrdIso( E , (rank β ((πβπ)βπ)))) |
88 | 87 | dmeqd 5827 |
. . . . . . . . . . . . 13
β’ (π = π β dom OrdIso( E , (rank β ((πβπ)βπ))) = dom OrdIso( E , (rank β ((πβπ)βπ)))) |
89 | 88 | eleq1d 2821 |
. . . . . . . . . . . 12
β’ (π = π β (dom OrdIso( E , (rank β
((πβπ)βπ))) β (π»βπ) β dom OrdIso( E , (rank β
((πβπ)βπ))) β (π»βπ))) |
90 | | simpll 765 |
. . . . . . . . . . . 12
β’
(((βπ β
π dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ) β§ (π β Ο β§ π β π)) β§ π β π) β βπ β π dom OrdIso( E , (rank β ((πβπ)βπ))) β (π»βπ)) |
91 | 46 | ssrab3 4021 |
. . . . . . . . . . . . . . . . . 18
β’ π β βͺ (π
1 β On) |
92 | 91 | sseli 3922 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β π β βͺ
(π
1 β On)) |
93 | | r1elssi 9611 |
. . . . . . . . . . . . . . . . 17
β’ (π β βͺ (π
1 β On) β π β βͺ (π
1 β On)) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β π β βͺ
(π
1 β On)) |
95 | 94 | sselda 3926 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β π) β π β βͺ
(π
1 β On)) |
96 | | snssi 4747 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β {π} β π) |
97 | 40 | tcss 9550 |
. . . . . . . . . . . . . . . . . . 19
β’ ({π} β π β (TCβ{π}) β (TCβπ)) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β (TCβ{π}) β (TCβπ)) |
99 | 49 | tcel 9551 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {π} β (TCβπ) β (TCβ{π})) |
100 | 52, 99 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β (TCβπ) β (TCβ{π})) |
101 | 98, 100 | sstrd 3936 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (TCβ{π}) β (TCβ{π})) |
102 | | ssralv 3992 |
. . . . . . . . . . . . . . . . 17
β’
((TCβ{π})
β (TCβ{π})
β (βπ β
(TCβ{π})π βΌ π β βπ β (TCβ{π})π βΌ π)) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (βπ β (TCβ{π})π βΌ π β βπ β (TCβ{π})π βΌ π)) |
104 | 48, 103 | mpan9 508 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β π) β βπ β (TCβ{π})π βΌ π) |
105 | | sneq 4575 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β {π} = {π}) |
106 | 105 | fveq2d 6808 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (TCβ{π}) = (TCβ{π})) |
107 | 106 | raleqdv 3367 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (βπ β (TCβ{π})π βΌ π β βπ β (TCβ{π})π βΌ π)) |
108 | 107, 46 | elrab2 3632 |
. . . . . . . . . . . . . . 15
β’ (π β π β (π β βͺ
(π
1 β On) β§ βπ β (TCβ{π})π βΌ π)) |
109 | 95, 104, 108 | sylanbrc 584 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β π β π) |
110 | 109 | adantll 712 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ π β π) β§ π β π) β π β π) |
111 | 110 | adantll 712 |
. . . . . . . . . . . 12
β’
(((βπ β
π dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ) β§ (π β Ο β§ π β π)) β§ π β π) β π β π) |
112 | 89, 90, 111 | rspcdva 3567 |
. . . . . . . . . . 11
β’
(((βπ β
π dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ) β§ (π β Ο β§ π β π)) β§ π β π) β dom OrdIso( E , (rank β
((πβπ)βπ))) β (π»βπ)) |
113 | | imassrn 5990 |
. . . . . . . . . . . . 13
β’ (rank
β ((πβπ)βπ)) β ran rank |
114 | 113, 32 | sstri 3935 |
. . . . . . . . . . . 12
β’ (rank
β ((πβπ)βπ)) β On |
115 | | fvex 6817 |
. . . . . . . . . . . . . . 15
β’ ((πβπ)βπ) β V |
116 | 115 | funimaex 6551 |
. . . . . . . . . . . . . 14
β’ (Fun rank
β (rank β ((πβπ)βπ)) β V) |
117 | 39, 116 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (rank
β ((πβπ)βπ)) β V |
118 | 117 | elpw 4543 |
. . . . . . . . . . . 12
β’ ((rank
β ((πβπ)βπ)) β π« On β (rank β
((πβπ)βπ)) β On) |
119 | 114, 118 | mpbir 230 |
. . . . . . . . . . 11
β’ (rank
β ((πβπ)βπ)) β π« On |
120 | 112, 119 | jctil 521 |
. . . . . . . . . 10
β’
(((βπ β
π dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ) β§ (π β Ο β§ π β π)) β§ π β π) β ((rank β ((πβπ)βπ)) β π« On β§ dom OrdIso( E ,
(rank β ((πβπ)βπ))) β (π»βπ))) |
121 | 120 | ralrimiva 3140 |
. . . . . . . . 9
β’
((βπ β
π dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ) β§ (π β Ο β§ π β π)) β βπ β π ((rank β ((πβπ)βπ)) β π« On β§ dom OrdIso( E ,
(rank β ((πβπ)βπ))) β (π»βπ))) |
122 | | eqid 2736 |
. . . . . . . . . 10
β’ OrdIso( E
, (rank β ((πβπ)βπ))) = OrdIso( E , (rank β ((πβπ)βπ))) |
123 | | eqid 2736 |
. . . . . . . . . 10
β’ OrdIso( E
, βͺ π β π (rank β ((πβπ)βπ))) = OrdIso( E , βͺ π β π (rank β ((πβπ)βπ))) |
124 | 122, 123 | hsmexlem3 10234 |
. . . . . . . . 9
β’ (((π βΌ* π β§ (π»βπ) β On) β§ βπ β π ((rank β ((πβπ)βπ)) β π« On β§ dom OrdIso( E ,
(rank β ((πβπ)βπ))) β (π»βπ))) β dom OrdIso( E , βͺ π β π (rank β ((πβπ)βπ))) β (harβπ« (π Γ (π»βπ)))) |
125 | 80, 82, 121, 124 | syl21anc 836 |
. . . . . . . 8
β’
((βπ β
π dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ) β§ (π β Ο β§ π β π)) β dom OrdIso( E , βͺ π β π (rank β ((πβπ)βπ))) β (harβπ« (π Γ (π»βπ)))) |
126 | 79, 125 | eqeltrid 2841 |
. . . . . . 7
β’
((βπ β
π dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ) β§ (π β Ο β§ π β π)) β dom OrdIso( E , (rank β
((πβπ)βsuc π))) β (harβπ« (π Γ (π»βπ)))) |
127 | 65 | hsmexlem8 10230 |
. . . . . . . 8
β’ (π β Ο β (π»βsuc π) = (harβπ« (π Γ (π»βπ)))) |
128 | 127 | ad2antrl 726 |
. . . . . . 7
β’
((βπ β
π dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ) β§ (π β Ο β§ π β π)) β (π»βsuc π) = (harβπ« (π Γ (π»βπ)))) |
129 | 126, 128 | eleqtrrd 2840 |
. . . . . 6
β’
((βπ β
π dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ) β§ (π β Ο β§ π β π)) β dom OrdIso( E , (rank β
((πβπ)βsuc π))) β (π»βsuc π)) |
130 | 129 | expr 458 |
. . . . 5
β’
((βπ β
π dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ) β§ π β Ο) β (π β π β dom OrdIso( E , (rank β
((πβπ)βsuc π))) β (π»βsuc π))) |
131 | 71, 130 | ralrimi 3237 |
. . . 4
β’
((βπ β
π dom OrdIso( E , (rank
β ((πβπ)βπ))) β (π»βπ) β§ π β Ο) β βπ β π dom OrdIso( E , (rank β ((πβπ)βsuc π))) β (π»βsuc π)) |
132 | 131 | expcom 415 |
. . 3
β’ (π β Ο β
(βπ β π dom OrdIso( E , (rank β
((πβπ)βπ))) β (π»βπ) β βπ β π dom OrdIso( E , (rank β ((πβπ)βsuc π))) β (π»βsuc π))) |
133 | 10, 19, 28, 68, 132 | finds1 7780 |
. 2
β’ (π β Ο β
βπ β π dom π β (π»βπ)) |
134 | 133 | r19.21bi 3231 |
1
β’ ((π β Ο β§ π β π) β dom π β (π»βπ)) |