Step | Hyp | Ref
| Expression |
1 | | wuncval2.f |
. . . 4
β’ πΉ = (rec((π§ β V β¦ ((π§ βͺ βͺ π§) βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ
Ο) |
2 | | wuncval2.u |
. . . 4
β’ π = βͺ
ran πΉ |
3 | 1, 2 | wunex2 10679 |
. . 3
β’ (π΄ β π β (π β WUni β§ π΄ β π)) |
4 | | wuncss 10686 |
. . 3
β’ ((π β WUni β§ π΄ β π) β (wUniClβπ΄) β π) |
5 | 3, 4 | syl 17 |
. 2
β’ (π΄ β π β (wUniClβπ΄) β π) |
6 | | frfnom 8382 |
. . . . . 6
β’
(rec((π§ β V
β¦ ((π§ βͺ βͺ π§)
βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ Ο) Fn
Ο |
7 | 1 | fneq1i 6600 |
. . . . . 6
β’ (πΉ Fn Ο β (rec((π§ β V β¦ ((π§ βͺ βͺ π§)
βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ Ο) Fn
Ο) |
8 | 6, 7 | mpbir 230 |
. . . . 5
β’ πΉ Fn Ο |
9 | | fniunfv 7195 |
. . . . 5
β’ (πΉ Fn Ο β βͺ π β Ο (πΉβπ) = βͺ ran πΉ) |
10 | 8, 9 | ax-mp 5 |
. . . 4
β’ βͺ π β Ο (πΉβπ) = βͺ ran πΉ |
11 | 2, 10 | eqtr4i 2764 |
. . 3
β’ π = βͺ π β Ο (πΉβπ) |
12 | | fveq2 6843 |
. . . . . . . 8
β’ (π = β
β (πΉβπ) = (πΉββ
)) |
13 | 12 | sseq1d 3976 |
. . . . . . 7
β’ (π = β
β ((πΉβπ) β (wUniClβπ΄) β (πΉββ
) β (wUniClβπ΄))) |
14 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (πΉβπ) = (πΉβπ)) |
15 | 14 | sseq1d 3976 |
. . . . . . 7
β’ (π = π β ((πΉβπ) β (wUniClβπ΄) β (πΉβπ) β (wUniClβπ΄))) |
16 | | fveq2 6843 |
. . . . . . . 8
β’ (π = suc π β (πΉβπ) = (πΉβsuc π)) |
17 | 16 | sseq1d 3976 |
. . . . . . 7
β’ (π = suc π β ((πΉβπ) β (wUniClβπ΄) β (πΉβsuc π) β (wUniClβπ΄))) |
18 | | 1on 8425 |
. . . . . . . . . 10
β’
1o β On |
19 | | unexg 7684 |
. . . . . . . . . 10
β’ ((π΄ β π β§ 1o β On) β
(π΄ βͺ 1o)
β V) |
20 | 18, 19 | mpan2 690 |
. . . . . . . . 9
β’ (π΄ β π β (π΄ βͺ 1o) β
V) |
21 | 1 | fveq1i 6844 |
. . . . . . . . . 10
β’ (πΉββ
) = ((rec((π§ β V β¦ ((π§ βͺ βͺ π§)
βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ
Ο)ββ
) |
22 | | fr0g 8383 |
. . . . . . . . . 10
β’ ((π΄ βͺ 1o) β V
β ((rec((π§ β V
β¦ ((π§ βͺ βͺ π§)
βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ
Ο)ββ
) = (π΄ βͺ 1o)) |
23 | 21, 22 | eqtrid 2785 |
. . . . . . . . 9
β’ ((π΄ βͺ 1o) β V
β (πΉββ
) =
(π΄ βͺ
1o)) |
24 | 20, 23 | syl 17 |
. . . . . . . 8
β’ (π΄ β π β (πΉββ
) = (π΄ βͺ 1o)) |
25 | | wuncid 10684 |
. . . . . . . . 9
β’ (π΄ β π β π΄ β (wUniClβπ΄)) |
26 | | df1o2 8420 |
. . . . . . . . . 10
β’
1o = {β
} |
27 | | wunccl 10685 |
. . . . . . . . . . . 12
β’ (π΄ β π β (wUniClβπ΄) β WUni) |
28 | 27 | wun0 10659 |
. . . . . . . . . . 11
β’ (π΄ β π β β
β (wUniClβπ΄)) |
29 | 28 | snssd 4770 |
. . . . . . . . . 10
β’ (π΄ β π β {β
} β
(wUniClβπ΄)) |
30 | 26, 29 | eqsstrid 3993 |
. . . . . . . . 9
β’ (π΄ β π β 1o β
(wUniClβπ΄)) |
31 | 25, 30 | unssd 4147 |
. . . . . . . 8
β’ (π΄ β π β (π΄ βͺ 1o) β
(wUniClβπ΄)) |
32 | 24, 31 | eqsstrd 3983 |
. . . . . . 7
β’ (π΄ β π β (πΉββ
) β (wUniClβπ΄)) |
33 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β π β Ο) |
34 | | fvex 6856 |
. . . . . . . . . . . . 13
β’ (πΉβπ) β V |
35 | 34 | uniex 7679 |
. . . . . . . . . . . . 13
β’ βͺ (πΉβπ) β V |
36 | 34, 35 | unex 7681 |
. . . . . . . . . . . 12
β’ ((πΉβπ) βͺ βͺ (πΉβπ)) β V |
37 | | prex 5390 |
. . . . . . . . . . . . . 14
β’
{π« π’, βͺ π’}
β V |
38 | 34 | mptex 7174 |
. . . . . . . . . . . . . . 15
β’ (π£ β (πΉβπ) β¦ {π’, π£}) β V |
39 | 38 | rnex 7850 |
. . . . . . . . . . . . . 14
β’ ran
(π£ β (πΉβπ) β¦ {π’, π£}) β V |
40 | 37, 39 | unex 7681 |
. . . . . . . . . . . . 13
β’
({π« π’, βͺ π’}
βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β V |
41 | 34, 40 | iunex 7902 |
. . . . . . . . . . . 12
β’ βͺ π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β V |
42 | 36, 41 | unex 7681 |
. . . . . . . . . . 11
β’ (((πΉβπ) βͺ βͺ (πΉβπ)) βͺ βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£}))) β V |
43 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π€ = π§ β π€ = π§) |
44 | | unieq 4877 |
. . . . . . . . . . . . . 14
β’ (π€ = π§ β βͺ π€ = βͺ
π§) |
45 | 43, 44 | uneq12d 4125 |
. . . . . . . . . . . . 13
β’ (π€ = π§ β (π€ βͺ βͺ π€) = (π§ βͺ βͺ π§)) |
46 | | pweq 4575 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = π₯ β π« π’ = π« π₯) |
47 | | unieq 4877 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = π₯ β βͺ π’ = βͺ
π₯) |
48 | 46, 47 | preq12d 4703 |
. . . . . . . . . . . . . . . 16
β’ (π’ = π₯ β {π« π’, βͺ π’} = {π« π₯, βͺ
π₯}) |
49 | | preq1 4695 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = π₯ β {π’, π£} = {π₯, π£}) |
50 | 49 | mpteq2dv 5208 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = π₯ β (π£ β π€ β¦ {π’, π£}) = (π£ β π€ β¦ {π₯, π£})) |
51 | 50 | rneqd 5894 |
. . . . . . . . . . . . . . . 16
β’ (π’ = π₯ β ran (π£ β π€ β¦ {π’, π£}) = ran (π£ β π€ β¦ {π₯, π£})) |
52 | 48, 51 | uneq12d 4125 |
. . . . . . . . . . . . . . 15
β’ (π’ = π₯ β ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£})) = ({π« π₯, βͺ π₯} βͺ ran (π£ β π€ β¦ {π₯, π£}))) |
53 | 52 | cbviunv 5001 |
. . . . . . . . . . . . . 14
β’ βͺ π’ β π€ ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£})) = βͺ
π₯ β π€ ({π« π₯, βͺ π₯} βͺ ran (π£ β π€ β¦ {π₯, π£})) |
54 | | preq2 4696 |
. . . . . . . . . . . . . . . . . . 19
β’ (π£ = π¦ β {π₯, π£} = {π₯, π¦}) |
55 | 54 | cbvmptv 5219 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ β π€ β¦ {π₯, π£}) = (π¦ β π€ β¦ {π₯, π¦}) |
56 | | mpteq1 5199 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ = π§ β (π¦ β π€ β¦ {π₯, π¦}) = (π¦ β π§ β¦ {π₯, π¦})) |
57 | 55, 56 | eqtrid 2785 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π§ β (π£ β π€ β¦ {π₯, π£}) = (π¦ β π§ β¦ {π₯, π¦})) |
58 | 57 | rneqd 5894 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π§ β ran (π£ β π€ β¦ {π₯, π£}) = ran (π¦ β π§ β¦ {π₯, π¦})) |
59 | 58 | uneq2d 4124 |
. . . . . . . . . . . . . . 15
β’ (π€ = π§ β ({π« π₯, βͺ π₯} βͺ ran (π£ β π€ β¦ {π₯, π£})) = ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦}))) |
60 | 43, 59 | iuneq12d 4983 |
. . . . . . . . . . . . . 14
β’ (π€ = π§ β βͺ
π₯ β π€ ({π« π₯, βͺ π₯} βͺ ran (π£ β π€ β¦ {π₯, π£})) = βͺ
π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦}))) |
61 | 53, 60 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ (π€ = π§ β βͺ
π’ β π€ ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£})) = βͺ
π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦}))) |
62 | 45, 61 | uneq12d 4125 |
. . . . . . . . . . . 12
β’ (π€ = π§ β ((π€ βͺ βͺ π€) βͺ βͺ π’ β π€ ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£}))) = ((π§ βͺ βͺ π§) βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))) |
63 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π€ = (πΉβπ) β π€ = (πΉβπ)) |
64 | | unieq 4877 |
. . . . . . . . . . . . . 14
β’ (π€ = (πΉβπ) β βͺ π€ = βͺ
(πΉβπ)) |
65 | 63, 64 | uneq12d 4125 |
. . . . . . . . . . . . 13
β’ (π€ = (πΉβπ) β (π€ βͺ βͺ π€) = ((πΉβπ) βͺ βͺ (πΉβπ))) |
66 | | mpteq1 5199 |
. . . . . . . . . . . . . . . 16
β’ (π€ = (πΉβπ) β (π£ β π€ β¦ {π’, π£}) = (π£ β (πΉβπ) β¦ {π’, π£})) |
67 | 66 | rneqd 5894 |
. . . . . . . . . . . . . . 15
β’ (π€ = (πΉβπ) β ran (π£ β π€ β¦ {π’, π£}) = ran (π£ β (πΉβπ) β¦ {π’, π£})) |
68 | 67 | uneq2d 4124 |
. . . . . . . . . . . . . 14
β’ (π€ = (πΉβπ) β ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£})) = ({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£}))) |
69 | 63, 68 | iuneq12d 4983 |
. . . . . . . . . . . . 13
β’ (π€ = (πΉβπ) β βͺ
π’ β π€ ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£})) = βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£}))) |
70 | 65, 69 | uneq12d 4125 |
. . . . . . . . . . . 12
β’ (π€ = (πΉβπ) β ((π€ βͺ βͺ π€) βͺ βͺ π’ β π€ ({π« π’, βͺ π’} βͺ ran (π£ β π€ β¦ {π’, π£}))) = (((πΉβπ) βͺ βͺ (πΉβπ)) βͺ βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})))) |
71 | 1, 62, 70 | frsucmpt2 8387 |
. . . . . . . . . . 11
β’ ((π β Ο β§ (((πΉβπ) βͺ βͺ (πΉβπ)) βͺ βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£}))) β V) β (πΉβsuc π) = (((πΉβπ) βͺ βͺ (πΉβπ)) βͺ βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})))) |
72 | 33, 42, 71 | sylancl 587 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β (πΉβsuc π) = (((πΉβπ) βͺ βͺ (πΉβπ)) βͺ βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})))) |
73 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β (πΉβπ) β (wUniClβπ΄)) |
74 | 27 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β (wUniClβπ΄) β WUni) |
75 | 73 | sselda 3945 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β π’ β (wUniClβπ΄)) |
76 | 74, 75 | wunelss 10649 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β π’ β (wUniClβπ΄)) |
77 | 76 | ralrimiva 3140 |
. . . . . . . . . . . . 13
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β βπ’ β (πΉβπ)π’ β (wUniClβπ΄)) |
78 | | unissb 4901 |
. . . . . . . . . . . . 13
β’ (βͺ (πΉβπ) β (wUniClβπ΄) β βπ’ β (πΉβπ)π’ β (wUniClβπ΄)) |
79 | 77, 78 | sylibr 233 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β βͺ
(πΉβπ) β (wUniClβπ΄)) |
80 | 73, 79 | unssd 4147 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β ((πΉβπ) βͺ βͺ (πΉβπ)) β (wUniClβπ΄)) |
81 | 74, 75 | wunpw 10648 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β π« π’ β (wUniClβπ΄)) |
82 | 74, 75 | wununi 10647 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β βͺ π’ β (wUniClβπ΄)) |
83 | 81, 82 | prssd 4783 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β {π« π’, βͺ π’} β (wUniClβπ΄)) |
84 | 74 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β§ π£ β (πΉβπ)) β (wUniClβπ΄) β WUni) |
85 | 75 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β§ π£ β (πΉβπ)) β π’ β (wUniClβπ΄)) |
86 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β (πΉβπ) β (wUniClβπ΄)) |
87 | 86 | sselda 3945 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β§ π£ β (πΉβπ)) β π£ β (wUniClβπ΄)) |
88 | 84, 85, 87 | wunpr 10650 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β§ π£ β (πΉβπ)) β {π’, π£} β (wUniClβπ΄)) |
89 | 88 | fmpttd 7064 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β (π£ β (πΉβπ) β¦ {π’, π£}):(πΉβπ)βΆ(wUniClβπ΄)) |
90 | 89 | frnd 6677 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β ran (π£ β (πΉβπ) β¦ {π’, π£}) β (wUniClβπ΄)) |
91 | 83, 90 | unssd 4147 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β§ π’ β (πΉβπ)) β ({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β (wUniClβπ΄)) |
92 | 91 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β βπ’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β (wUniClβπ΄)) |
93 | | iunss 5006 |
. . . . . . . . . . . 12
β’ (βͺ π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β (wUniClβπ΄) β βπ’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β (wUniClβπ΄)) |
94 | 92, 93 | sylibr 233 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β βͺ π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£})) β (wUniClβπ΄)) |
95 | 80, 94 | unssd 4147 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β (((πΉβπ) βͺ βͺ (πΉβπ)) βͺ βͺ
π’ β (πΉβπ)({π« π’, βͺ π’} βͺ ran (π£ β (πΉβπ) β¦ {π’, π£}))) β (wUniClβπ΄)) |
96 | 72, 95 | eqsstrd 3983 |
. . . . . . . . 9
β’ (((π΄ β π β§ π β Ο) β§ (πΉβπ) β (wUniClβπ΄)) β (πΉβsuc π) β (wUniClβπ΄)) |
97 | 96 | ex 414 |
. . . . . . . 8
β’ ((π΄ β π β§ π β Ο) β ((πΉβπ) β (wUniClβπ΄) β (πΉβsuc π) β (wUniClβπ΄))) |
98 | 97 | expcom 415 |
. . . . . . 7
β’ (π β Ο β (π΄ β π β ((πΉβπ) β (wUniClβπ΄) β (πΉβsuc π) β (wUniClβπ΄)))) |
99 | 13, 15, 17, 32, 98 | finds2 7838 |
. . . . . 6
β’ (π β Ο β (π΄ β π β (πΉβπ) β (wUniClβπ΄))) |
100 | 99 | com12 32 |
. . . . 5
β’ (π΄ β π β (π β Ο β (πΉβπ) β (wUniClβπ΄))) |
101 | 100 | ralrimiv 3139 |
. . . 4
β’ (π΄ β π β βπ β Ο (πΉβπ) β (wUniClβπ΄)) |
102 | | iunss 5006 |
. . . 4
β’ (βͺ π β Ο (πΉβπ) β (wUniClβπ΄) β βπ β Ο (πΉβπ) β (wUniClβπ΄)) |
103 | 101, 102 | sylibr 233 |
. . 3
β’ (π΄ β π β βͺ
π β Ο (πΉβπ) β (wUniClβπ΄)) |
104 | 11, 103 | eqsstrid 3993 |
. 2
β’ (π΄ β π β π β (wUniClβπ΄)) |
105 | 5, 104 | eqssd 3962 |
1
β’ (π΄ β π β (wUniClβπ΄) = π) |