Step | Hyp | Ref
| Expression |
1 | | wuncval2.f |
. . . 4
β’ πΉ = (rec((π§ β V β¦ ((π§ βͺ βͺ π§) βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ
Ο) |
2 | | wuncval2.u |
. . . 4
β’ π = βͺ
ran πΉ |
3 | 1, 2 | wunex2 10735 |
. . 3
β’ (π΄ β π β (π β WUni β§ π΄ β π)) |
4 | | wuncss 10742 |
. . 3
β’ ((π β WUni β§ π΄ β π) β (wUniClβπ΄) β π) |
5 | 3, 4 | syl 17 |
. 2
β’ (π΄ β π β (wUniClβπ΄) β π) |
6 | | frfnom 8437 |
. . . . . 6
β’
(rec((π§ β V
β¦ ((π§ βͺ βͺ π§)
βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ Ο) Fn
Ο |
7 | 1 | fneq1i 6645 |
. . . . . 6
β’ (πΉ Fn Ο β (rec((π§ β V β¦ ((π§ βͺ βͺ π§)
βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ Ο) Fn
Ο) |
8 | 6, 7 | mpbir 230 |
. . . . 5
β’ πΉ Fn Ο |
9 | | fniunfv 7248 |
. . . . 5
β’ (πΉ Fn Ο β βͺ π β Ο (πΉβπ) = βͺ ran πΉ) |
10 | 8, 9 | ax-mp 5 |
. . . 4
β’ βͺ π β Ο (πΉβπ) = βͺ ran πΉ |
11 | 2, 10 | eqtr4i 2761 |
. . 3
β’ π = βͺ π β Ο (πΉβπ) |
12 | | fveq2 6890 |
. . . . . . . 8
β’ (π = β
β (πΉβπ) = (πΉββ
)) |
13 | 12 | sseq1d 4012 |
. . . . . . 7
β’ (π = β
β ((πΉβπ) β (wUniClβπ΄) β (πΉββ
) β (wUniClβπ΄))) |
14 | | fveq2 6890 |
. . . . . . . 8
β’ (π = π β (πΉβπ) = (πΉβπ)) |
15 | 14 | sseq1d 4012 |
. . . . . . 7
β’ (π = π β ((πΉβπ) β (wUniClβπ΄) β (πΉβπ) β (wUniClβπ΄))) |
16 | | fveq2 6890 |
. . . . . . . 8
β’ (π = suc π β (πΉβπ) = (πΉβsuc π)) |
17 | 16 | sseq1d 4012 |
. . . . . . 7
β’ (π = suc π β ((πΉβπ) β (wUniClβπ΄) β (πΉβsuc π) β (wUniClβπ΄))) |
18 | | 1on 8480 |
. . . . . . . . . 10
β’
1o β On |
19 | | unexg 7738 |
. . . . . . . . . 10
β’ ((π΄ β π β§ 1o β On) β
(π΄ βͺ 1o)
β V) |
20 | 18, 19 | mpan2 687 |
. . . . . . . . 9
β’ (π΄ β π β (π΄ βͺ 1o) β
V) |
21 | 1 | fveq1i 6891 |
. . . . . . . . . 10
β’ (πΉββ
) = ((rec((π§ β V β¦ ((π§ βͺ βͺ π§)
βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ
Ο)ββ
) |
22 | | fr0g 8438 |
. . . . . . . . . 10
β’ ((π΄ βͺ 1o) β V
β ((rec((π§ β V
β¦ ((π§ βͺ βͺ π§)
βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ
Ο)ββ
) = (π΄ βͺ 1o)) |
23 | 21, 22 | eqtrid 2782 |
. . . . . . . . 9
β’ ((π΄ βͺ 1o) β V
β (πΉββ
) =
(π΄ βͺ
1o)) |
24 | 20, 23 | syl 17 |
. . . . . . . 8
β’ (π΄ β π β (πΉββ
) = (π΄ βͺ 1o)) |
25 | | wuncid 10740 |
. . . . . . . . 9
β’ (π΄ β π β π΄ β (wUniClβπ΄)) |
26 | | df1o2 8475 |
. . . . . . . . . 10
β’
1o = {β
} |
27 | | wunccl 10741 |
. . . . . . . . . . . 12
β’ (π΄ β π β (wUniClβπ΄) β WUni) |
28 | 27 | wun0 10715 |
. . . . . . . . . . 11
β’ (π΄ β π β β
β (wUniClβπ΄)) |
29 | 28 | snssd 4811 |
. . . . . . . . . 10
β’ (π΄ β π β {β
} β
(wUniClβπ΄)) |
30 | 26, 29 | eqsstrid 4029 |
. . . . . . . . 9
β’ (π΄ β π β 1o β
(wUniClβπ΄)) |
31 | 25, 30 | unssd 4185 |
. . . . . . . 8
β’ (π΄ β π β (π΄ βͺ 1o) β
(wUniClβπ΄)) |
32 | 24, 31 | eqsstrd 4019 |
. . . . . . 7
β’ (π΄ β π β (πΉββ
) β (wUniClβπ΄)) |
33 | | simplr 765 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β π β Ο) |
34 | | fvex 6903 |
. . . . . . . . . . . . 13
β’ (πΉβπ) β V |
35 | 34 | uniex 7733 |
. . . . . . . . . . . . 13
β’ βͺ (πΉβπ) β V |
36 | 34, 35 | unex 7735 |
. . . . . . . . . . . 12
β’ ((πΉβπ) βͺ βͺ (πΉβπ)) β V |
37 | | prex 5431 |
. . . . . . . . . . . . . 14
β’
{π« π’, βͺ π’}
β V |
38 | 34 | mptex 7226 |
. . . . . . . . . . . . . . 15
β’ (π£ β (πΉβπ) β¦ {π’, π£}) β V |
39 | 38 | rnex 7905 |
. . . . . . . . . . . . . 14
β’ ran
(π£ β (πΉβπ) β¦ {π’, π£}) β V |
40 | 37, 39 | unex 7735 |
. . . . . . . . . . . . 13
β’
({π« π’, βͺ π’}
βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β V |
41 | 34, 40 | iunex 7957 |
. . . . . . . . . . . 12
β’ βͺ π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β V |
42 | 36, 41 | unex 7735 |
. . . . . . . . . . 11
β’ (((πΉβπ) βͺ βͺ (πΉβπ)) βͺ βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£}))) β V |
43 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π€ = π§ β π€ = π§) |
44 | | unieq 4918 |
. . . . . . . . . . . . . 14
β’ (π€ = π§ β βͺ π€ = βͺ
π§) |
45 | 43, 44 | uneq12d 4163 |
. . . . . . . . . . . . 13
β’ (π€ = π§ β (π€ βͺ βͺ π€) = (π§ βͺ βͺ π§)) |
46 | | pweq 4615 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = π₯ β π« π’ = π« π₯) |
47 | | unieq 4918 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = π₯ β βͺ π’ = βͺ
π₯) |
48 | 46, 47 | preq12d 4744 |
. . . . . . . . . . . . . . . 16
β’ (π’ = π₯ β {π« π’, βͺ π’} = {π« π₯, βͺ
π₯}) |
49 | | preq1 4736 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = π₯ β {π’, π£} = {π₯, π£}) |
50 | 49 | mpteq2dv 5249 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = π₯ β (π£ β π€ β¦ {π’, π£}) = (π£ β π€ β¦ {π₯, π£})) |
51 | 50 | rneqd 5936 |
. . . . . . . . . . . . . . . 16
β’ (π’ = π₯ β ran (π£ β π€ β¦ {π’, π£}) = ran (π£ β π€ β¦ {π₯, π£})) |
52 | 48, 51 | uneq12d 4163 |
. . . . . . . . . . . . . . 15
β’ (π’ = π₯ β ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£})) = ({π« π₯, βͺ π₯} βͺ ran (π£ β π€ β¦ {π₯, π£}))) |
53 | 52 | cbviunv 5042 |
. . . . . . . . . . . . . 14
β’ βͺ π’ β π€ ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£})) = βͺ
π₯ β π€ ({π« π₯, βͺ π₯} βͺ ran (π£ β π€ β¦ {π₯, π£})) |
54 | | preq2 4737 |
. . . . . . . . . . . . . . . . . . 19
β’ (π£ = π¦ β {π₯, π£} = {π₯, π¦}) |
55 | 54 | cbvmptv 5260 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ β π€ β¦ {π₯, π£}) = (π¦ β π€ β¦ {π₯, π¦}) |
56 | | mpteq1 5240 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ = π§ β (π¦ β π€ β¦ {π₯, π¦}) = (π¦ β π§ β¦ {π₯, π¦})) |
57 | 55, 56 | eqtrid 2782 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π§ β (π£ β π€ β¦ {π₯, π£}) = (π¦ β π§ β¦ {π₯, π¦})) |
58 | 57 | rneqd 5936 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π§ β ran (π£ β π€ β¦ {π₯, π£}) = ran (π¦ β π§ β¦ {π₯, π¦})) |
59 | 58 | uneq2d 4162 |
. . . . . . . . . . . . . . 15
β’ (π€ = π§ β ({π« π₯, βͺ π₯} βͺ ran (π£ β π€ β¦ {π₯, π£})) = ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦}))) |
60 | 43, 59 | iuneq12d 5024 |
. . . . . . . . . . . . . 14
β’ (π€ = π§ β βͺ
π₯ β π€ ({π« π₯, βͺ π₯} βͺ ran (π£ β π€ β¦ {π₯, π£})) = βͺ
π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦}))) |
61 | 53, 60 | eqtrid 2782 |
. . . . . . . . . . . . 13
β’ (π€ = π§ β βͺ
π’ β π€ ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£})) = βͺ
π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦}))) |
62 | 45, 61 | uneq12d 4163 |
. . . . . . . . . . . 12
β’ (π€ = π§ β ((π€ βͺ βͺ π€) βͺ βͺ π’ β π€ ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£}))) = ((π§ βͺ βͺ π§) βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))) |
63 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π€ = (πΉβπ) β π€ = (πΉβπ)) |
64 | | unieq 4918 |
. . . . . . . . . . . . . 14
β’ (π€ = (πΉβπ) β βͺ π€ = βͺ
(πΉβπ)) |
65 | 63, 64 | uneq12d 4163 |
. . . . . . . . . . . . 13
β’ (π€ = (πΉβπ) β (π€ βͺ βͺ π€) = ((πΉβπ) βͺ βͺ (πΉβπ))) |
66 | | mpteq1 5240 |
. . . . . . . . . . . . . . . 16
β’ (π€ = (πΉβπ) β (π£ β π€ β¦ {π’, π£}) = (π£ β (πΉβπ) β¦ {π’, π£})) |
67 | 66 | rneqd 5936 |
. . . . . . . . . . . . . . 15
β’ (π€ = (πΉβπ) β ran (π£ β π€ β¦ {π’, π£}) = ran (π£ β (πΉβπ) β¦ {π’, π£})) |
68 | 67 | uneq2d 4162 |
. . . . . . . . . . . . . 14
β’ (π€ = (πΉβπ) β ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£})) = ({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£}))) |
69 | 63, 68 | iuneq12d 5024 |
. . . . . . . . . . . . 13
β’ (π€ = (πΉβπ) β βͺ
π’ β π€ ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£})) = βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£}))) |
70 | 65, 69 | uneq12d 4163 |
. . . . . . . . . . . 12
β’ (π€ = (πΉβπ) β ((π€ βͺ βͺ π€) βͺ βͺ π’ β π€ ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£}))) = (((πΉβπ) βͺ βͺ (πΉβπ)) βͺ βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})))) |
71 | 1, 62, 70 | frsucmpt2 8442 |
. . . . . . . . . . 11
β’ ((π β Ο β§ (((πΉβπ) βͺ βͺ (πΉβπ)) βͺ βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£}))) β V) β (πΉβsuc π) = (((πΉβπ) βͺ βͺ (πΉβπ)) βͺ βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})))) |
72 | 33, 42, 71 | sylancl 584 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β (πΉβsuc π) = (((πΉβπ) βͺ βͺ (πΉβπ)) βͺ βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})))) |
73 | | simpr 483 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β (πΉβπ) β (wUniClβπ΄)) |
74 | 27 | ad3antrrr 726 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β (wUniClβπ΄) β WUni) |
75 | 73 | sselda 3981 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β π’ β (wUniClβπ΄)) |
76 | 74, 75 | wunelss 10705 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β π’ β (wUniClβπ΄)) |
77 | 76 | ralrimiva 3144 |
. . . . . . . . . . . . 13
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β βπ’ β (πΉβπ)π’ β (wUniClβπ΄)) |
78 | | unissb 4942 |
. . . . . . . . . . . . 13
β’ (βͺ (πΉβπ) β (wUniClβπ΄) β βπ’ β (πΉβπ)π’ β (wUniClβπ΄)) |
79 | 77, 78 | sylibr 233 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β βͺ
(πΉβπ) β (wUniClβπ΄)) |
80 | 73, 79 | unssd 4185 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β ((πΉβπ) βͺ βͺ (πΉβπ)) β (wUniClβπ΄)) |
81 | 74, 75 | wunpw 10704 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β π« π’ β (wUniClβπ΄)) |
82 | 74, 75 | wununi 10703 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β βͺ π’ β (wUniClβπ΄)) |
83 | 81, 82 | prssd 4824 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β {π« π’, βͺ π’} β (wUniClβπ΄)) |
84 | 74 | adantr 479 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β§ π£ β (πΉβπ)) β (wUniClβπ΄) β WUni) |
85 | 75 | adantr 479 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β§ π£ β (πΉβπ)) β π’ β (wUniClβπ΄)) |
86 | | simplr 765 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β (πΉβπ) β (wUniClβπ΄)) |
87 | 86 | sselda 3981 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β§ π£ β (πΉβπ)) β π£ β (wUniClβπ΄)) |
88 | 84, 85, 87 | wunpr 10706 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β§ π£ β (πΉβπ)) β {π’, π£} β (wUniClβπ΄)) |
89 | 88 | fmpttd 7115 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β (π£ β (πΉβπ) β¦ {π’, π£}):(πΉβπ)βΆ(wUniClβπ΄)) |
90 | 89 | frnd 6724 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β ran (π£ β (πΉβπ) β¦ {π’, π£}) β (wUniClβπ΄)) |
91 | 83, 90 | unssd 4185 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β ({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β (wUniClβπ΄)) |
92 | 91 | ralrimiva 3144 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β βπ’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β (wUniClβπ΄)) |
93 | | iunss 5047 |
. . . . . . . . . . . 12
β’ (βͺ π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β (wUniClβπ΄) β βπ’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β (wUniClβπ΄)) |
94 | 92, 93 | sylibr 233 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β βͺ π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β (wUniClβπ΄)) |
95 | 80, 94 | unssd 4185 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β (((πΉβπ) βͺ βͺ (πΉβπ)) βͺ βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£}))) β (wUniClβπ΄)) |
96 | 72, 95 | eqsstrd 4019 |
. . . . . . . . 9
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β (πΉβsuc π) β (wUniClβπ΄)) |
97 | 96 | ex 411 |
. . . . . . . 8
β’ ((π΄ β π β§ π β Ο) β ((πΉβπ) β (wUniClβπ΄) β (πΉβsuc π) β (wUniClβπ΄))) |
98 | 97 | expcom 412 |
. . . . . . 7
β’ (π β Ο β (π΄ β π β ((πΉβπ) β (wUniClβπ΄) β (πΉβsuc π) β (wUniClβπ΄)))) |
99 | 13, 15, 17, 32, 98 | finds2 7893 |
. . . . . 6
β’ (π β Ο β (π΄ β π β (πΉβπ) β (wUniClβπ΄))) |
100 | 99 | com12 32 |
. . . . 5
β’ (π΄ β π β (π β Ο β (πΉβπ) β (wUniClβπ΄))) |
101 | 100 | ralrimiv 3143 |
. . . 4
β’ (π΄ β π β βπ β Ο (πΉβπ) β (wUniClβπ΄)) |
102 | | iunss 5047 |
. . . 4
β’ (βͺ π β Ο (πΉβπ) β (wUniClβπ΄) β βπ β Ο (πΉβπ) β (wUniClβπ΄)) |
103 | 101, 102 | sylibr 233 |
. . 3
β’ (π΄ β π β βͺ
π β Ο (πΉβπ) β (wUniClβπ΄)) |
104 | 11, 103 | eqsstrid 4029 |
. 2
β’ (π΄ β π β π β (wUniClβπ΄)) |
105 | 5, 104 | eqssd 3998 |
1
β’ (π΄ β π β (wUniClβπ΄) = π) |