Step | Hyp | Ref
| Expression |
1 | | brdomi 8904 |
. . . 4
β’ (Ο
βΌ π΄ β
βπ π:Οβ1-1βπ΄) |
2 | 1 | adantr 482 |
. . 3
β’ ((Ο
βΌ π΄ β§ π΅ β π΄) β βπ π:Οβ1-1βπ΄) |
3 | | reldom 8895 |
. . . . . . 7
β’ Rel
βΌ |
4 | 3 | brrelex2i 5693 |
. . . . . 6
β’ (Ο
βΌ π΄ β π΄ β V) |
5 | 4 | ad2antrr 725 |
. . . . 5
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π΄ β V) |
6 | | simplr 768 |
. . . . 5
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π΅ β π΄) |
7 | | f1f 6742 |
. . . . . . 7
β’ (π:Οβ1-1βπ΄ β π:ΟβΆπ΄) |
8 | 7 | adantl 483 |
. . . . . 6
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π:ΟβΆπ΄) |
9 | | peano1 7829 |
. . . . . 6
β’ β
β Ο |
10 | | ffvelcdm 7036 |
. . . . . 6
β’ ((π:ΟβΆπ΄ β§ β
β Ο)
β (πββ
)
β π΄) |
11 | 8, 9, 10 | sylancl 587 |
. . . . 5
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (πββ
) β π΄) |
12 | | difsnen 9003 |
. . . . 5
β’ ((π΄ β V β§ π΅ β π΄ β§ (πββ
) β π΄) β (π΄ β {π΅}) β (π΄ β {(πββ
)})) |
13 | 5, 6, 11, 12 | syl3anc 1372 |
. . . 4
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π΄ β {π΅}) β (π΄ β {(πββ
)})) |
14 | | vex 3451 |
. . . . . . . . . 10
β’ π β V |
15 | | f1f1orn 6799 |
. . . . . . . . . . 11
β’ (π:Οβ1-1βπ΄ β π:Οβ1-1-ontoβran
π) |
16 | 15 | adantl 483 |
. . . . . . . . . 10
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π:Οβ1-1-ontoβran
π) |
17 | | f1oen3g 8912 |
. . . . . . . . . 10
β’ ((π β V β§ π:Οβ1-1-ontoβran
π) β Ο β
ran π) |
18 | 14, 16, 17 | sylancr 588 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β Ο β ran π) |
19 | 18 | ensymd 8951 |
. . . . . . . 8
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ran π β Ο) |
20 | 3 | brrelex1i 5692 |
. . . . . . . . . . 11
β’ (Ο
βΌ π΄ β Ο
β V) |
21 | 20 | ad2antrr 725 |
. . . . . . . . . 10
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β Ο β V) |
22 | | limom 7822 |
. . . . . . . . . . 11
β’ Lim
Ο |
23 | 22 | limenpsi 9102 |
. . . . . . . . . 10
β’ (Ο
β V β Ο β (Ο β {β
})) |
24 | 21, 23 | syl 17 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β Ο β (Ο β
{β
})) |
25 | 14 | resex 5989 |
. . . . . . . . . . 11
β’ (π βΎ (Ο β
{β
})) β V |
26 | | simpr 486 |
. . . . . . . . . . . 12
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π:Οβ1-1βπ΄) |
27 | | difss 4095 |
. . . . . . . . . . . 12
β’ (Ο
β {β
}) β Ο |
28 | | f1ores 6802 |
. . . . . . . . . . . 12
β’ ((π:Οβ1-1βπ΄ β§ (Ο β {β
}) β
Ο) β (π βΎ
(Ο β {β
})):(Ο β {β
})β1-1-ontoβ(π β (Ο β
{β
}))) |
29 | 26, 27, 28 | sylancl 587 |
. . . . . . . . . . 11
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π βΎ (Ο β
{β
})):(Ο β {β
})β1-1-ontoβ(π β (Ο β
{β
}))) |
30 | | f1oen3g 8912 |
. . . . . . . . . . 11
β’ (((π βΎ (Ο β
{β
})) β V β§ (π βΎ (Ο β
{β
})):(Ο β {β
})β1-1-ontoβ(π β (Ο β {β
}))) β
(Ο β {β
}) β (π β (Ο β
{β
}))) |
31 | 25, 29, 30 | sylancr 588 |
. . . . . . . . . 10
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (Ο β {β
}) β
(π β (Ο β
{β
}))) |
32 | | f1orn 6798 |
. . . . . . . . . . . . 13
β’ (π:Οβ1-1-ontoβran
π β (π Fn Ο β§ Fun β‘π)) |
33 | 32 | simprbi 498 |
. . . . . . . . . . . 12
β’ (π:Οβ1-1-ontoβran
π β Fun β‘π) |
34 | | imadif 6589 |
. . . . . . . . . . . 12
β’ (Fun
β‘π β (π β (Ο β {β
})) =
((π β Ο)
β (π β
{β
}))) |
35 | 16, 33, 34 | 3syl 18 |
. . . . . . . . . . 11
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π β (Ο β {β
})) =
((π β Ο)
β (π β
{β
}))) |
36 | | f1fn 6743 |
. . . . . . . . . . . . . 14
β’ (π:Οβ1-1βπ΄ β π Fn Ο) |
37 | 36 | adantl 483 |
. . . . . . . . . . . . 13
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π Fn Ο) |
38 | | fnima 6635 |
. . . . . . . . . . . . 13
β’ (π Fn Ο β (π β Ο) = ran π) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π β Ο) = ran π) |
40 | | fnsnfv 6924 |
. . . . . . . . . . . . . 14
β’ ((π Fn Ο β§ β
β
Ο) β {(πββ
)} = (π β {β
})) |
41 | 37, 9, 40 | sylancl 587 |
. . . . . . . . . . . . 13
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β {(πββ
)} = (π β {β
})) |
42 | 41 | eqcomd 2739 |
. . . . . . . . . . . 12
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π β {β
}) = {(πββ
)}) |
43 | 39, 42 | difeq12d 4087 |
. . . . . . . . . . 11
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((π β Ο) β (π β {β
})) = (ran π β {(πββ
)})) |
44 | 35, 43 | eqtrd 2773 |
. . . . . . . . . 10
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π β (Ο β {β
})) = (ran
π β {(πββ
)})) |
45 | 31, 44 | breqtrd 5135 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (Ο β {β
}) β
(ran π β {(πββ
)})) |
46 | | entr 8952 |
. . . . . . . . 9
β’ ((Ο
β (Ο β {β
}) β§ (Ο β {β
}) β
(ran π β {(πββ
)})) β
Ο β (ran π
β {(πββ
)})) |
47 | 24, 45, 46 | syl2anc 585 |
. . . . . . . 8
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β Ο β (ran π β {(πββ
)})) |
48 | | entr 8952 |
. . . . . . . 8
β’ ((ran
π β Ο β§
Ο β (ran π
β {(πββ
)})) β ran π β (ran π β {(πββ
)})) |
49 | 19, 47, 48 | syl2anc 585 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ran π β (ran π β {(πββ
)})) |
50 | | difexg 5288 |
. . . . . . . 8
β’ (π΄ β V β (π΄ β ran π) β V) |
51 | | enrefg 8930 |
. . . . . . . 8
β’ ((π΄ β ran π) β V β (π΄ β ran π) β (π΄ β ran π)) |
52 | 5, 50, 51 | 3syl 18 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π΄ β ran π) β (π΄ β ran π)) |
53 | | disjdif 4435 |
. . . . . . . 8
β’ (ran
π β© (π΄ β ran π)) = β
|
54 | 53 | a1i 11 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (ran π β© (π΄ β ran π)) = β
) |
55 | | difss 4095 |
. . . . . . . . . 10
β’ (ran
π β {(πββ
)}) β ran
π |
56 | | ssrin 4197 |
. . . . . . . . . 10
β’ ((ran
π β {(πββ
)}) β ran
π β ((ran π β {(πββ
)}) β© (π΄ β ran π)) β (ran π β© (π΄ β ran π))) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . 9
β’ ((ran
π β {(πββ
)}) β© (π΄ β ran π)) β (ran π β© (π΄ β ran π)) |
58 | | sseq0 4363 |
. . . . . . . . 9
β’ ((((ran
π β {(πββ
)}) β© (π΄ β ran π)) β (ran π β© (π΄ β ran π)) β§ (ran π β© (π΄ β ran π)) = β
) β ((ran π β {(πββ
)}) β© (π΄ β ran π)) = β
) |
59 | 57, 53, 58 | mp2an 691 |
. . . . . . . 8
β’ ((ran
π β {(πββ
)}) β© (π΄ β ran π)) = β
|
60 | 59 | a1i 11 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((ran π β {(πββ
)}) β© (π΄ β ran π)) = β
) |
61 | | unen 8996 |
. . . . . . 7
β’ (((ran
π β (ran π β {(πββ
)}) β§ (π΄ β ran π) β (π΄ β ran π)) β§ ((ran π β© (π΄ β ran π)) = β
β§ ((ran π β {(πββ
)}) β© (π΄ β ran π)) = β
)) β (ran π βͺ (π΄ β ran π)) β ((ran π β {(πββ
)}) βͺ (π΄ β ran π))) |
62 | 49, 52, 54, 60, 61 | syl22anc 838 |
. . . . . 6
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (ran π βͺ (π΄ β ran π)) β ((ran π β {(πββ
)}) βͺ (π΄ β ran π))) |
63 | 8 | frnd 6680 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ran π β π΄) |
64 | | undif 4445 |
. . . . . . 7
β’ (ran
π β π΄ β (ran π βͺ (π΄ β ran π)) = π΄) |
65 | 63, 64 | sylib 217 |
. . . . . 6
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (ran π βͺ (π΄ β ran π)) = π΄) |
66 | | uncom 4117 |
. . . . . . 7
β’ ((ran
π β {(πββ
)}) βͺ (π΄ β ran π)) = ((π΄ β ran π) βͺ (ran π β {(πββ
)})) |
67 | | eldifn 4091 |
. . . . . . . . . . 11
β’ ((πββ
) β (π΄ β ran π) β Β¬ (πββ
) β ran π) |
68 | | fnfvelrn 7035 |
. . . . . . . . . . . 12
β’ ((π Fn Ο β§ β
β
Ο) β (πββ
) β ran π) |
69 | 37, 9, 68 | sylancl 587 |
. . . . . . . . . . 11
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (πββ
) β ran π) |
70 | 67, 69 | nsyl3 138 |
. . . . . . . . . 10
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β Β¬ (πββ
) β (π΄ β ran π)) |
71 | | disjsn 4676 |
. . . . . . . . . 10
β’ (((π΄ β ran π) β© {(πββ
)}) = β
β Β¬
(πββ
) β
(π΄ β ran π)) |
72 | 70, 71 | sylibr 233 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((π΄ β ran π) β© {(πββ
)}) = β
) |
73 | | undif4 4430 |
. . . . . . . . 9
β’ (((π΄ β ran π) β© {(πββ
)}) = β
β ((π΄ β ran π) βͺ (ran π β {(πββ
)})) = (((π΄ β ran π) βͺ ran π) β {(πββ
)})) |
74 | 72, 73 | syl 17 |
. . . . . . . 8
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((π΄ β ran π) βͺ (ran π β {(πββ
)})) = (((π΄ β ran π) βͺ ran π) β {(πββ
)})) |
75 | | uncom 4117 |
. . . . . . . . . 10
β’ ((π΄ β ran π) βͺ ran π) = (ran π βͺ (π΄ β ran π)) |
76 | 75, 65 | eqtrid 2785 |
. . . . . . . . 9
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((π΄ β ran π) βͺ ran π) = π΄) |
77 | 76 | difeq1d 4085 |
. . . . . . . 8
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (((π΄ β ran π) βͺ ran π) β {(πββ
)}) = (π΄ β {(πββ
)})) |
78 | 74, 77 | eqtrd 2773 |
. . . . . . 7
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((π΄ β ran π) βͺ (ran π β {(πββ
)})) = (π΄ β {(πββ
)})) |
79 | 66, 78 | eqtrid 2785 |
. . . . . 6
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β ((ran π β {(πββ
)}) βͺ (π΄ β ran π)) = (π΄ β {(πββ
)})) |
80 | 62, 65, 79 | 3brtr3d 5140 |
. . . . 5
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β π΄ β (π΄ β {(πββ
)})) |
81 | 80 | ensymd 8951 |
. . . 4
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π΄ β {(πββ
)}) β π΄) |
82 | | entr 8952 |
. . . 4
β’ (((π΄ β {π΅}) β (π΄ β {(πββ
)}) β§ (π΄ β {(πββ
)}) β π΄) β (π΄ β {π΅}) β π΄) |
83 | 13, 81, 82 | syl2anc 585 |
. . 3
β’
(((Ο βΌ π΄
β§ π΅ β π΄) β§ π:Οβ1-1βπ΄) β (π΄ β {π΅}) β π΄) |
84 | 2, 83 | exlimddv 1939 |
. 2
β’ ((Ο
βΌ π΄ β§ π΅ β π΄) β (π΄ β {π΅}) β π΄) |
85 | | difsn 4762 |
. . . 4
β’ (Β¬
π΅ β π΄ β (π΄ β {π΅}) = π΄) |
86 | 85 | adantl 483 |
. . 3
β’ ((Ο
βΌ π΄ β§ Β¬ π΅ β π΄) β (π΄ β {π΅}) = π΄) |
87 | | enrefg 8930 |
. . . . 5
β’ (π΄ β V β π΄ β π΄) |
88 | 4, 87 | syl 17 |
. . . 4
β’ (Ο
βΌ π΄ β π΄ β π΄) |
89 | 88 | adantr 482 |
. . 3
β’ ((Ο
βΌ π΄ β§ Β¬ π΅ β π΄) β π΄ β π΄) |
90 | 86, 89 | eqbrtrd 5131 |
. 2
β’ ((Ο
βΌ π΄ β§ Β¬ π΅ β π΄) β (π΄ β {π΅}) β π΄) |
91 | 84, 90 | pm2.61dan 812 |
1
β’ (Ο
βΌ π΄ β (π΄ β {π΅}) β π΄) |