Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . 3
β’ (π΅ = β
β (π΄ βm π΅) = (π΄ βm
β
)) |
2 | | breq2 5114 |
. . . . 5
β’ (π΅ = β
β (π₯ β π΅ β π₯ β β
)) |
3 | 2 | anbi2d 630 |
. . . 4
β’ (π΅ = β
β ((π₯ β π΄ β§ π₯ β π΅) β (π₯ β π΄ β§ π₯ β β
))) |
4 | 3 | abbidv 2806 |
. . 3
β’ (π΅ = β
β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} = {π₯ β£ (π₯ β π΄ β§ π₯ β β
)}) |
5 | 1, 4 | breq12d 5123 |
. 2
β’ (π΅ = β
β ((π΄ βm π΅) β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} β (π΄ βm β
) β {π₯ β£ (π₯ β π΄ β§ π₯ β β
)})) |
6 | | simpl2 1193 |
. . . . . . . . . 10
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β π΅ βΌ π΄) |
7 | | reldom 8896 |
. . . . . . . . . . 11
β’ Rel
βΌ |
8 | 7 | brrelex1i 5693 |
. . . . . . . . . 10
β’ (π΅ βΌ π΄ β π΅ β V) |
9 | 6, 8 | syl 17 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β π΅ β V) |
10 | 7 | brrelex2i 5694 |
. . . . . . . . . 10
β’ (π΅ βΌ π΄ β π΄ β V) |
11 | 6, 10 | syl 17 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β π΄ β V) |
12 | | xpcomeng 9015 |
. . . . . . . . 9
β’ ((π΅ β V β§ π΄ β V) β (π΅ Γ π΄) β (π΄ Γ π΅)) |
13 | 9, 11, 12 | syl2anc 585 |
. . . . . . . 8
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β (π΅ Γ π΄) β (π΄ Γ π΅)) |
14 | | simpl3 1194 |
. . . . . . . . . 10
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β (π΄ βm π΅) β dom card) |
15 | | simpr 486 |
. . . . . . . . . . 11
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β π΅ β β
) |
16 | | mapdom3 9100 |
. . . . . . . . . . 11
β’ ((π΄ β V β§ π΅ β V β§ π΅ β β
) β π΄ βΌ (π΄ βm π΅)) |
17 | 11, 9, 15, 16 | syl3anc 1372 |
. . . . . . . . . 10
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β π΄ βΌ (π΄ βm π΅)) |
18 | | numdom 9981 |
. . . . . . . . . 10
β’ (((π΄ βm π΅) β dom card β§ π΄ βΌ (π΄ βm π΅)) β π΄ β dom card) |
19 | 14, 17, 18 | syl2anc 585 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β π΄ β dom card) |
20 | | simpl1 1192 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β Ο βΌ π΄) |
21 | | infxpabs 10155 |
. . . . . . . . 9
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ (π΅ β β
β§ π΅ βΌ π΄)) β (π΄ Γ π΅) β π΄) |
22 | 19, 20, 15, 6, 21 | syl22anc 838 |
. . . . . . . 8
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β (π΄ Γ π΅) β π΄) |
23 | | entr 8953 |
. . . . . . . 8
β’ (((π΅ Γ π΄) β (π΄ Γ π΅) β§ (π΄ Γ π΅) β π΄) β (π΅ Γ π΄) β π΄) |
24 | 13, 22, 23 | syl2anc 585 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β (π΅ Γ π΄) β π΄) |
25 | | ssenen 9102 |
. . . . . . 7
β’ ((π΅ Γ π΄) β π΄ β {π₯ β£ (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)} β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)}) |
26 | 24, 25 | syl 17 |
. . . . . 6
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β {π₯ β£ (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)} β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)}) |
27 | | relen 8895 |
. . . . . . 7
β’ Rel
β |
28 | 27 | brrelex1i 5693 |
. . . . . 6
β’ ({π₯ β£ (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)} β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} β {π₯ β£ (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)} β V) |
29 | 26, 28 | syl 17 |
. . . . 5
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β {π₯ β£ (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)} β V) |
30 | | abid2 2876 |
. . . . . 6
β’ {π₯ β£ π₯ β (π΄ βm π΅)} = (π΄ βm π΅) |
31 | | elmapi 8794 |
. . . . . . . 8
β’ (π₯ β (π΄ βm π΅) β π₯:π΅βΆπ΄) |
32 | | fssxp 6701 |
. . . . . . . . 9
β’ (π₯:π΅βΆπ΄ β π₯ β (π΅ Γ π΄)) |
33 | | ffun 6676 |
. . . . . . . . . . 11
β’ (π₯:π΅βΆπ΄ β Fun π₯) |
34 | | vex 3452 |
. . . . . . . . . . . 12
β’ π₯ β V |
35 | 34 | fundmen 8982 |
. . . . . . . . . . 11
β’ (Fun
π₯ β dom π₯ β π₯) |
36 | | ensym 8950 |
. . . . . . . . . . 11
β’ (dom
π₯ β π₯ β π₯ β dom π₯) |
37 | 33, 35, 36 | 3syl 18 |
. . . . . . . . . 10
β’ (π₯:π΅βΆπ΄ β π₯ β dom π₯) |
38 | | fdm 6682 |
. . . . . . . . . 10
β’ (π₯:π΅βΆπ΄ β dom π₯ = π΅) |
39 | 37, 38 | breqtrd 5136 |
. . . . . . . . 9
β’ (π₯:π΅βΆπ΄ β π₯ β π΅) |
40 | 32, 39 | jca 513 |
. . . . . . . 8
β’ (π₯:π΅βΆπ΄ β (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)) |
41 | 31, 40 | syl 17 |
. . . . . . 7
β’ (π₯ β (π΄ βm π΅) β (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)) |
42 | 41 | ss2abi 4028 |
. . . . . 6
β’ {π₯ β£ π₯ β (π΄ βm π΅)} β {π₯ β£ (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)} |
43 | 30, 42 | eqsstrri 3984 |
. . . . 5
β’ (π΄ βm π΅) β {π₯ β£ (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)} |
44 | | ssdomg 8947 |
. . . . 5
β’ ({π₯ β£ (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)} β V β ((π΄ βm π΅) β {π₯ β£ (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)} β (π΄ βm π΅) βΌ {π₯ β£ (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)})) |
45 | 29, 43, 44 | mpisyl 21 |
. . . 4
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β (π΄ βm π΅) βΌ {π₯ β£ (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)}) |
46 | | domentr 8960 |
. . . 4
β’ (((π΄ βm π΅) βΌ {π₯ β£ (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)} β§ {π₯ β£ (π₯ β (π΅ Γ π΄) β§ π₯ β π΅)} β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)}) β (π΄ βm π΅) βΌ {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)}) |
47 | 45, 26, 46 | syl2anc 585 |
. . 3
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β (π΄ βm π΅) βΌ {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)}) |
48 | | ovex 7395 |
. . . . . . 7
β’ (π΄ βm π΅) β V |
49 | 48 | mptex 7178 |
. . . . . 6
β’ (π β (π΄ βm π΅) β¦ ran π) β V |
50 | 49 | rnex 7854 |
. . . . 5
β’ ran
(π β (π΄ βm π΅) β¦ ran π) β V |
51 | | ensym 8950 |
. . . . . . . . . . . 12
β’ (π₯ β π΅ β π΅ β π₯) |
52 | 51 | ad2antll 728 |
. . . . . . . . . . 11
β’
((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β π΅ β π₯) |
53 | | bren 8900 |
. . . . . . . . . . 11
β’ (π΅ β π₯ β βπ π:π΅β1-1-ontoβπ₯) |
54 | 52, 53 | sylib 217 |
. . . . . . . . . 10
β’
((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β βπ π:π΅β1-1-ontoβπ₯) |
55 | | f1of 6789 |
. . . . . . . . . . . . . . . 16
β’ (π:π΅β1-1-ontoβπ₯ β π:π΅βΆπ₯) |
56 | 55 | adantl 483 |
. . . . . . . . . . . . . . 15
β’
(((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β§ π:π΅β1-1-ontoβπ₯) β π:π΅βΆπ₯) |
57 | | simplrl 776 |
. . . . . . . . . . . . . . 15
β’
(((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β§ π:π΅β1-1-ontoβπ₯) β π₯ β π΄) |
58 | 56, 57 | fssd 6691 |
. . . . . . . . . . . . . 14
β’
(((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β§ π:π΅β1-1-ontoβπ₯) β π:π΅βΆπ΄) |
59 | 11, 9 | elmapd 8786 |
. . . . . . . . . . . . . . 15
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β (π β (π΄ βm π΅) β π:π΅βΆπ΄)) |
60 | 59 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β§ π:π΅β1-1-ontoβπ₯) β (π β (π΄ βm π΅) β π:π΅βΆπ΄)) |
61 | 58, 60 | mpbird 257 |
. . . . . . . . . . . . 13
β’
(((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β§ π:π΅β1-1-ontoβπ₯) β π β (π΄ βm π΅)) |
62 | | f1ofo 6796 |
. . . . . . . . . . . . . . . 16
β’ (π:π΅β1-1-ontoβπ₯ β π:π΅βontoβπ₯) |
63 | | forn 6764 |
. . . . . . . . . . . . . . . 16
β’ (π:π΅βontoβπ₯ β ran π = π₯) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π:π΅β1-1-ontoβπ₯ β ran π = π₯) |
65 | 64 | adantl 483 |
. . . . . . . . . . . . . 14
β’
(((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β§ π:π΅β1-1-ontoβπ₯) β ran π = π₯) |
66 | 65 | eqcomd 2743 |
. . . . . . . . . . . . 13
β’
(((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β§ π:π΅β1-1-ontoβπ₯) β π₯ = ran π) |
67 | 61, 66 | jca 513 |
. . . . . . . . . . . 12
β’
(((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β§ π:π΅β1-1-ontoβπ₯) β (π β (π΄ βm π΅) β§ π₯ = ran π)) |
68 | 67 | ex 414 |
. . . . . . . . . . 11
β’
((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β (π:π΅β1-1-ontoβπ₯ β (π β (π΄ βm π΅) β§ π₯ = ran π))) |
69 | 68 | eximdv 1921 |
. . . . . . . . . 10
β’
((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β (βπ π:π΅β1-1-ontoβπ₯ β βπ(π β (π΄ βm π΅) β§ π₯ = ran π))) |
70 | 54, 69 | mpd 15 |
. . . . . . . . 9
β’
((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β βπ(π β (π΄ βm π΅) β§ π₯ = ran π)) |
71 | | df-rex 3075 |
. . . . . . . . 9
β’
(βπ β
(π΄ βm π΅)π₯ = ran π β βπ(π β (π΄ βm π΅) β§ π₯ = ran π)) |
72 | 70, 71 | sylibr 233 |
. . . . . . . 8
β’
((((Ο βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β§ (π₯ β π΄ β§ π₯ β π΅)) β βπ β (π΄ βm π΅)π₯ = ran π) |
73 | 72 | ex 414 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β ((π₯ β π΄ β§ π₯ β π΅) β βπ β (π΄ βm π΅)π₯ = ran π)) |
74 | 73 | ss2abdv 4025 |
. . . . . 6
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} β {π₯ β£ βπ β (π΄ βm π΅)π₯ = ran π}) |
75 | | eqid 2737 |
. . . . . . 7
β’ (π β (π΄ βm π΅) β¦ ran π) = (π β (π΄ βm π΅) β¦ ran π) |
76 | 75 | rnmpt 5915 |
. . . . . 6
β’ ran
(π β (π΄ βm π΅) β¦ ran π) = {π₯ β£ βπ β (π΄ βm π΅)π₯ = ran π} |
77 | 74, 76 | sseqtrrdi 4000 |
. . . . 5
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} β ran (π β (π΄ βm π΅) β¦ ran π)) |
78 | | ssdomg 8947 |
. . . . 5
β’ (ran
(π β (π΄ βm π΅) β¦ ran π) β V β ({π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} β ran (π β (π΄ βm π΅) β¦ ran π) β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} βΌ ran (π β (π΄ βm π΅) β¦ ran π))) |
79 | 50, 77, 78 | mpsyl 68 |
. . . 4
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} βΌ ran (π β (π΄ βm π΅) β¦ ran π)) |
80 | | vex 3452 |
. . . . . . . . 9
β’ π β V |
81 | 80 | rnex 7854 |
. . . . . . . 8
β’ ran π β V |
82 | 81 | rgenw 3069 |
. . . . . . 7
β’
βπ β
(π΄ βm π΅)ran π β V |
83 | 75 | fnmpt 6646 |
. . . . . . 7
β’
(βπ β
(π΄ βm π΅)ran π β V β (π β (π΄ βm π΅) β¦ ran π) Fn (π΄ βm π΅)) |
84 | 82, 83 | mp1i 13 |
. . . . . 6
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β (π β (π΄ βm π΅) β¦ ran π) Fn (π΄ βm π΅)) |
85 | | dffn4 6767 |
. . . . . 6
β’ ((π β (π΄ βm π΅) β¦ ran π) Fn (π΄ βm π΅) β (π β (π΄ βm π΅) β¦ ran π):(π΄ βm π΅)βontoβran (π β (π΄ βm π΅) β¦ ran π)) |
86 | 84, 85 | sylib 217 |
. . . . 5
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β (π β (π΄ βm π΅) β¦ ran π):(π΄ βm π΅)βontoβran (π β (π΄ βm π΅) β¦ ran π)) |
87 | | fodomnum 10000 |
. . . . 5
β’ ((π΄ βm π΅) β dom card β ((π β (π΄ βm π΅) β¦ ran π):(π΄ βm π΅)βontoβran (π β (π΄ βm π΅) β¦ ran π) β ran (π β (π΄ βm π΅) β¦ ran π) βΌ (π΄ βm π΅))) |
88 | 14, 86, 87 | sylc 65 |
. . . 4
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β ran (π β (π΄ βm π΅) β¦ ran π) βΌ (π΄ βm π΅)) |
89 | | domtr 8954 |
. . . 4
β’ (({π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} βΌ ran (π β (π΄ βm π΅) β¦ ran π) β§ ran (π β (π΄ βm π΅) β¦ ran π) βΌ (π΄ βm π΅)) β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} βΌ (π΄ βm π΅)) |
90 | 79, 88, 89 | syl2anc 585 |
. . 3
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} βΌ (π΄ βm π΅)) |
91 | | sbth 9044 |
. . 3
β’ (((π΄ βm π΅) βΌ {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} β§ {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)} βΌ (π΄ βm π΅)) β (π΄ βm π΅) β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)}) |
92 | 47, 90, 91 | syl2anc 585 |
. 2
β’
(((Ο βΌ π΄
β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β§ π΅ β β
) β (π΄ βm π΅) β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)}) |
93 | 7 | brrelex2i 5694 |
. . . . 5
β’ (Ο
βΌ π΄ β π΄ β V) |
94 | 93 | 3ad2ant1 1134 |
. . . 4
β’ ((Ο
βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β π΄ β V) |
95 | | map0e 8827 |
. . . 4
β’ (π΄ β V β (π΄ βm β
) =
1o) |
96 | 94, 95 | syl 17 |
. . 3
β’ ((Ο
βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β (π΄ βm β
) =
1o) |
97 | | 1oex 8427 |
. . . . 5
β’
1o β V |
98 | 97 | enref 8932 |
. . . 4
β’
1o β 1o |
99 | | df-sn 4592 |
. . . . 5
β’ {β
}
= {π₯ β£ π₯ = β
} |
100 | | df1o2 8424 |
. . . . 5
β’
1o = {β
} |
101 | | en0 8964 |
. . . . . . . 8
β’ (π₯ β β
β π₯ = β
) |
102 | 101 | anbi2i 624 |
. . . . . . 7
β’ ((π₯ β π΄ β§ π₯ β β
) β (π₯ β π΄ β§ π₯ = β
)) |
103 | | 0ss 4361 |
. . . . . . . . 9
β’ β
β π΄ |
104 | | sseq1 3974 |
. . . . . . . . 9
β’ (π₯ = β
β (π₯ β π΄ β β
β π΄)) |
105 | 103, 104 | mpbiri 258 |
. . . . . . . 8
β’ (π₯ = β
β π₯ β π΄) |
106 | 105 | pm4.71ri 562 |
. . . . . . 7
β’ (π₯ = β
β (π₯ β π΄ β§ π₯ = β
)) |
107 | 102, 106 | bitr4i 278 |
. . . . . 6
β’ ((π₯ β π΄ β§ π₯ β β
) β π₯ = β
) |
108 | 107 | abbii 2807 |
. . . . 5
β’ {π₯ β£ (π₯ β π΄ β§ π₯ β β
)} = {π₯ β£ π₯ = β
} |
109 | 99, 100, 108 | 3eqtr4ri 2776 |
. . . 4
β’ {π₯ β£ (π₯ β π΄ β§ π₯ β β
)} =
1o |
110 | 98, 109 | breqtrri 5137 |
. . 3
β’
1o β {π₯ β£ (π₯ β π΄ β§ π₯ β β
)} |
111 | 96, 110 | eqbrtrdi 5149 |
. 2
β’ ((Ο
βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β (π΄ βm β
) β {π₯ β£ (π₯ β π΄ β§ π₯ β β
)}) |
112 | 5, 92, 111 | pm2.61ne 3031 |
1
β’ ((Ο
βΌ π΄ β§ π΅ βΌ π΄ β§ (π΄ βm π΅) β dom card) β (π΄ βm π΅) β {π₯ β£ (π₯ β π΄ β§ π₯ β π΅)}) |