Step | Hyp | Ref
| Expression |
1 | | brdomi 8953 |
. . . 4
β’ (Ο
βΌ π΄ β
βπ π:Οβ1-1βπ΄) |
2 | 1 | adantr 481 |
. . 3
β’ ((Ο
βΌ π΄ β§ π΅ β π΄) β βπ π:Οβ1-1βπ΄) |
3 | | reldom 8944 |
. . . . . . 7
β’ Rel
βΌ |
4 | 3 | brrelex2i 5733 |
. . . . . 6
β’ (Ο
βΌ π΄ β π΄ β V) |
5 | 4 | ad2antrr 724 |
. . . . 5
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π΄ β V) |
6 | | simplr 767 |
. . . . 5
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π΅ β π΄) |
7 | | f1f 6787 |
. . . . . . 7
β’ (π:Οβ1-1βπ΄ β π:ΟβΆπ΄) |
8 | 7 | adantl 482 |
. . . . . 6
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π:ΟβΆπ΄) |
9 | | peano1 7878 |
. . . . . 6
β’ β
β Ο |
10 | | ffvelcdm 7083 |
. . . . . 6
β’ ((π:ΟβΆπ΄ β§ β
β Ο)
β (πββ
)
β π΄) |
11 | 8, 9, 10 | sylancl 586 |
. . . . 5
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (πββ
) β π΄) |
12 | | difsnen 9052 |
. . . . 5
β’ ((π΄ β V β§ π΅ β π΄ β§ (πββ
) β π΄) β (π΄ β {π΅}) β (π΄ β {(πββ
)})) |
13 | 5, 6, 11, 12 | syl3anc 1371 |
. . . 4
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π΄ β {π΅}) β (π΄ β {(πββ
)})) |
14 | | vex 3478 |
. . . . . . . . . 10
β’ π β V |
15 | | f1f1orn 6844 |
. . . . . . . . . . 11
β’ (π:Οβ1-1βπ΄ β π:Οβ1-1-ontoβran
π) |
16 | 15 | adantl 482 |
. . . . . . . . . 10
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π:Οβ1-1-ontoβran
π) |
17 | | f1oen3g 8961 |
. . . . . . . . . 10
β’ ((π β V β§ π:Οβ1-1-ontoβran
π) β Ο β
ran π) |
18 | 14, 16, 17 | sylancr 587 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β Ο β ran π) |
19 | 18 | ensymd 9000 |
. . . . . . . 8
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ran π β Ο) |
20 | 3 | brrelex1i 5732 |
. . . . . . . . . . 11
β’ (Ο
βΌ π΄ β Ο
β V) |
21 | 20 | ad2antrr 724 |
. . . . . . . . . 10
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β Ο β V) |
22 | | limom 7870 |
. . . . . . . . . . 11
β’ Lim
Ο |
23 | 22 | limenpsi 9151 |
. . . . . . . . . 10
β’ (Ο
β V β Ο β (Ο β {β
})) |
24 | 21, 23 | syl 17 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β Ο β (Ο β
{β
})) |
25 | 14 | resex 6029 |
. . . . . . . . . . 11
β’ (π βΎ (Ο β
{β
})) β V |
26 | | simpr 485 |
. . . . . . . . . . . 12
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π:Οβ1-1βπ΄) |
27 | | difss 4131 |
. . . . . . . . . . . 12
β’ (Ο
β {β
}) β Ο |
28 | | f1ores 6847 |
. . . . . . . . . . . 12
β’ ((π:Οβ1-1βπ΄ β§ (Ο β {β
}) β
Ο) β (π βΎ
(Ο β {β
})):(Ο β {β
})β1-1-ontoβ(π β (Ο β
{β
}))) |
29 | 26, 27, 28 | sylancl 586 |
. . . . . . . . . . 11
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π βΎ (Ο β
{β
})):(Ο β {β
})β1-1-ontoβ(π β (Ο β
{β
}))) |
30 | | f1oen3g 8961 |
. . . . . . . . . . 11
β’ (((π βΎ (Ο β
{β
})) β V β§ (π βΎ (Ο β
{β
})):(Ο β {β
})β1-1-ontoβ(π β (Ο β {β
}))) β
(Ο β {β
}) β (π β (Ο β
{β
}))) |
31 | 25, 29, 30 | sylancr 587 |
. . . . . . . . . 10
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (Ο β {β
}) β
(π β (Ο β
{β
}))) |
32 | | f1orn 6843 |
. . . . . . . . . . . . 13
β’ (π:Οβ1-1-ontoβran
π β (π Fn Ο β§ Fun β‘π)) |
33 | 32 | simprbi 497 |
. . . . . . . . . . . 12
β’ (π:Οβ1-1-ontoβran
π β Fun β‘π) |
34 | | imadif 6632 |
. . . . . . . . . . . 12
β’ (Fun
β‘π β (π β (Ο β {β
})) =
((π β Ο)
β (π β
{β
}))) |
35 | 16, 33, 34 | 3syl 18 |
. . . . . . . . . . 11
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π β (Ο β {β
})) =
((π β Ο)
β (π β
{β
}))) |
36 | | f1fn 6788 |
. . . . . . . . . . . . . 14
β’ (π:Οβ1-1βπ΄ β π Fn Ο) |
37 | 36 | adantl 482 |
. . . . . . . . . . . . 13
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π Fn Ο) |
38 | | fnima 6680 |
. . . . . . . . . . . . 13
β’ (π Fn Ο β (π β Ο) = ran π) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π β Ο) = ran π) |
40 | | fnsnfv 6970 |
. . . . . . . . . . . . . 14
β’ ((π Fn Ο β§ β
β
Ο) β {(πββ
)} = (π β {β
})) |
41 | 37, 9, 40 | sylancl 586 |
. . . . . . . . . . . . 13
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β {(πββ
)} = (π β {β
})) |
42 | 41 | eqcomd 2738 |
. . . . . . . . . . . 12
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π β {β
}) = {(πββ
)}) |
43 | 39, 42 | difeq12d 4123 |
. . . . . . . . . . 11
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((π β Ο) β (π β {β
})) = (ran π β {(πββ
)})) |
44 | 35, 43 | eqtrd 2772 |
. . . . . . . . . 10
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π β (Ο β {β
})) = (ran
π β {(πββ
)})) |
45 | 31, 44 | breqtrd 5174 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (Ο β {β
}) β
(ran π β {(πββ
)})) |
46 | | entr 9001 |
. . . . . . . . 9
β’ ((Ο
β (Ο β {β
}) β§ (Ο β {β
}) β
(ran π β {(πββ
)})) β
Ο β (ran π
β {(πββ
)})) |
47 | 24, 45, 46 | syl2anc 584 |
. . . . . . . 8
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β Ο β (ran π β {(πββ
)})) |
48 | | entr 9001 |
. . . . . . . 8
β’ ((ran
π β Ο β§
Ο β (ran π
β {(πββ
)})) β ran π β (ran π β {(πββ
)})) |
49 | 19, 47, 48 | syl2anc 584 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ran π β (ran π β {(πββ
)})) |
50 | | difexg 5327 |
. . . . . . . 8
β’ (π΄ β V β (π΄ β ran π) β V) |
51 | | enrefg 8979 |
. . . . . . . 8
β’ ((π΄ β ran π) β V β (π΄ β ran π) β (π΄ β ran π)) |
52 | 5, 50, 51 | 3syl 18 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π΄ β ran π) β (π΄ β ran π)) |
53 | | disjdif 4471 |
. . . . . . . 8
β’ (ran
π β© (π΄ β ran π)) = β
|
54 | 53 | a1i 11 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (ran π β© (π΄ β ran π)) = β
) |
55 | | difss 4131 |
. . . . . . . . . 10
β’ (ran
π β {(πββ
)}) β ran
π |
56 | | ssrin 4233 |
. . . . . . . . . 10
β’ ((ran
π β {(πββ
)}) β ran
π β ((ran π β {(πββ
)}) β© (π΄ β ran π)) β (ran π β© (π΄ β ran π))) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . 9
β’ ((ran
π β {(πββ
)}) β© (π΄ β ran π)) β (ran π β© (π΄ β ran π)) |
58 | | sseq0 4399 |
. . . . . . . . 9
β’ ((((ran
π β {(πββ
)}) β© (π΄ β ran π)) β (ran π β© (π΄ β ran π)) β§ (ran π β© (π΄ β ran π)) = β
) β ((ran π β {(πββ
)}) β© (π΄ β ran π)) = β
) |
59 | 57, 53, 58 | mp2an 690 |
. . . . . . . 8
β’ ((ran
π β {(πββ
)}) β© (π΄ β ran π)) = β
|
60 | 59 | a1i 11 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((ran π β {(πββ
)}) β© (π΄ β ran π)) = β
) |
61 | | unen 9045 |
. . . . . . 7
β’ (((ran
π β (ran π β {(πββ
)}) β§ (π΄ β ran π) β (π΄ β ran π)) β§ ((ran π β© (π΄ β ran π)) = β
β§ ((ran π β {(πββ
)}) β© (π΄ β ran π)) = β
)) β (ran π βͺ (π΄ β ran π)) β ((ran π β {(πββ
)}) βͺ (π΄ β ran π))) |
62 | 49, 52, 54, 60, 61 | syl22anc 837 |
. . . . . 6
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (ran π βͺ (π΄ β ran π)) β ((ran π β {(πββ
)}) βͺ (π΄ β ran π))) |
63 | 8 | frnd 6725 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ran π β π΄) |
64 | | undif 4481 |
. . . . . . 7
β’ (ran
π β π΄ β (ran π βͺ (π΄ β ran π)) = π΄) |
65 | 63, 64 | sylib 217 |
. . . . . 6
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (ran π βͺ (π΄ β ran π)) = π΄) |
66 | | uncom 4153 |
. . . . . . 7
β’ ((ran
π β {(πββ
)}) βͺ (π΄ β ran π)) = ((π΄ β ran π) βͺ (ran π β {(πββ
)})) |
67 | | eldifn 4127 |
. . . . . . . . . . 11
β’ ((πββ
) β (π΄ β ran π) β Β¬ (πββ
) β ran π) |
68 | | fnfvelrn 7082 |
. . . . . . . . . . . 12
β’ ((π Fn Ο β§ β
β
Ο) β (πββ
) β ran π) |
69 | 37, 9, 68 | sylancl 586 |
. . . . . . . . . . 11
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (πββ
) β ran π) |
70 | 67, 69 | nsyl3 138 |
. . . . . . . . . 10
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β Β¬ (πββ
) β (π΄ β ran π)) |
71 | | disjsn 4715 |
. . . . . . . . . 10
β’ (((π΄ β ran π) β© {(πββ
)}) = β
β Β¬
(πββ
) β
(π΄ β ran π)) |
72 | 70, 71 | sylibr 233 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((π΄ β ran π) β© {(πββ
)}) = β
) |
73 | | undif4 4466 |
. . . . . . . . 9
β’ (((π΄ β ran π) β© {(πββ
)}) = β
β ((π΄ β ran π) βͺ (ran π β {(πββ
)})) = (((π΄ β ran π) βͺ ran π) β {(πββ
)})) |
74 | 72, 73 | syl 17 |
. . . . . . . 8
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((π΄ β ran π) βͺ (ran π β {(πββ
)})) = (((π΄ β ran π) βͺ ran π) β {(πββ
)})) |
75 | | uncom 4153 |
. . . . . . . . . 10
β’ ((π΄ β ran π) βͺ ran π) = (ran π βͺ (π΄ β ran π)) |
76 | 75, 65 | eqtrid 2784 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((π΄ β ran π) βͺ ran π) = π΄) |
77 | 76 | difeq1d 4121 |
. . . . . . . 8
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (((π΄ β ran π) βͺ ran π) β {(πββ
)}) = (π΄ β {(πββ
)})) |
78 | 74, 77 | eqtrd 2772 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((π΄ β ran π) βͺ (ran π β {(πββ
)})) = (π΄ β {(πββ
)})) |
79 | 66, 78 | eqtrid 2784 |
. . . . . 6
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((ran π β {(πββ
)}) βͺ (π΄ β ran π)) = (π΄ β {(πββ
)})) |
80 | 62, 65, 79 | 3brtr3d 5179 |
. . . . 5
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π΄ β (π΄ β {(πββ
)})) |
81 | 80 | ensymd 9000 |
. . . 4
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π΄ β {(πββ
)}) β π΄) |
82 | | entr 9001 |
. . . 4
β’ (((π΄ β {π΅}) β (π΄ β {(πββ
)}) β§ (π΄ β {(πββ
)}) β π΄) β (π΄ β {π΅}) β π΄) |
83 | 13, 81, 82 | syl2anc 584 |
. . 3
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π΄ β {π΅}) β π΄) |
84 | 2, 83 | exlimddv 1938 |
. 2
β’ ((Ο
βΌ π΄ β§ π΅ β π΄) β (π΄ β {π΅}) β π΄) |
85 | | difsn 4801 |
. . . 4
β’ (Β¬
π΅ β π΄ β (π΄ β {π΅}) = π΄) |
86 | 85 | adantl 482 |
. . 3
β’ ((Ο
βΌ π΄ β§ Β¬ π΅ β π΄) β (π΄ β {π΅}) = π΄) |
87 | | enrefg 8979 |
. . . . 5
β’ (π΄ β V β π΄ β π΄) |
88 | 4, 87 | syl 17 |
. . . 4
β’ (Ο
βΌ π΄ β π΄ β π΄) |
89 | 88 | adantr 481 |
. . 3
β’ ((Ο
βΌ π΄ β§ Β¬ π΅ β π΄) β π΄ β π΄) |
90 | 86, 89 | eqbrtrd 5170 |
. 2
β’ ((Ο
βΌ π΄ β§ Β¬ π΅ β π΄) β (π΄ β {π΅}) β π΄) |
91 | 84, 90 | pm2.61dan 811 |
1
β’ (Ο
βΌ π΄ β (π΄ β {π΅}) β π΄) |