# Metamath Proof Explorer

## Theorem infdifsn

Description: Removing a singleton from an infinite set does not change the cardinality of the set. (Contributed by Mario Carneiro, 30-Apr-2015) (Revised by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion infdifsn ${⊢}\mathrm{\omega }\preccurlyeq {A}\to \left({A}\setminus \left\{{B}\right\}\right)\approx {A}$

### Proof

Step Hyp Ref Expression
1 brdomi ${⊢}\mathrm{\omega }\preccurlyeq {A}\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\mathrm{\omega }\underset{1-1}{⟶}{A}$
2 1 adantr ${⊢}\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\mathrm{\omega }\underset{1-1}{⟶}{A}$
3 reldom ${⊢}\mathrm{Rel}\preccurlyeq$
4 3 brrelex2i ${⊢}\mathrm{\omega }\preccurlyeq {A}\to {A}\in \mathrm{V}$
5 4 ad2antrr ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {A}\in \mathrm{V}$
6 simplr ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {B}\in {A}$
7 f1f ${⊢}{f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\to {f}:\mathrm{\omega }⟶{A}$
8 7 adantl ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {f}:\mathrm{\omega }⟶{A}$
9 peano1 ${⊢}\varnothing \in \mathrm{\omega }$
10 ffvelrn ${⊢}\left({f}:\mathrm{\omega }⟶{A}\wedge \varnothing \in \mathrm{\omega }\right)\to {f}\left(\varnothing \right)\in {A}$
11 8 9 10 sylancl ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {f}\left(\varnothing \right)\in {A}$
12 difsnen ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in {A}\wedge {f}\left(\varnothing \right)\in {A}\right)\to \left({A}\setminus \left\{{B}\right\}\right)\approx \left({A}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)$
13 5 6 11 12 syl3anc ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left({A}\setminus \left\{{B}\right\}\right)\approx \left({A}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)$
14 vex ${⊢}{f}\in \mathrm{V}$
15 f1f1orn ${⊢}{f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\to {f}:\mathrm{\omega }\underset{1-1 onto}{⟶}\mathrm{ran}{f}$
16 15 adantl ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {f}:\mathrm{\omega }\underset{1-1 onto}{⟶}\mathrm{ran}{f}$
17 f1oen3g ${⊢}\left({f}\in \mathrm{V}\wedge {f}:\mathrm{\omega }\underset{1-1 onto}{⟶}\mathrm{ran}{f}\right)\to \mathrm{\omega }\approx \mathrm{ran}{f}$
18 14 16 17 sylancr ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \mathrm{\omega }\approx \mathrm{ran}{f}$
19 18 ensymd ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \mathrm{ran}{f}\approx \mathrm{\omega }$
20 3 brrelex1i ${⊢}\mathrm{\omega }\preccurlyeq {A}\to \mathrm{\omega }\in \mathrm{V}$
21 20 ad2antrr ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \mathrm{\omega }\in \mathrm{V}$
22 limom ${⊢}\mathrm{Lim}\mathrm{\omega }$
23 22 limenpsi ${⊢}\mathrm{\omega }\in \mathrm{V}\to \mathrm{\omega }\approx \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)$
24 21 23 syl ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \mathrm{\omega }\approx \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)$
25 14 resex ${⊢}{{f}↾}_{\left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)}\in \mathrm{V}$
26 simpr ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}$
27 difss ${⊢}\mathrm{\omega }\setminus \left\{\varnothing \right\}\subseteq \mathrm{\omega }$
28 f1ores ${⊢}\left({f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\wedge \mathrm{\omega }\setminus \left\{\varnothing \right\}\subseteq \mathrm{\omega }\right)\to \left({{f}↾}_{\left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)}\right):\mathrm{\omega }\setminus \left\{\varnothing \right\}\underset{1-1 onto}{⟶}{f}\left[\mathrm{\omega }\setminus \left\{\varnothing \right\}\right]$
29 26 27 28 sylancl ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left({{f}↾}_{\left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)}\right):\mathrm{\omega }\setminus \left\{\varnothing \right\}\underset{1-1 onto}{⟶}{f}\left[\mathrm{\omega }\setminus \left\{\varnothing \right\}\right]$
30 f1oen3g ${⊢}\left({{f}↾}_{\left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)}\in \mathrm{V}\wedge \left({{f}↾}_{\left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)}\right):\mathrm{\omega }\setminus \left\{\varnothing \right\}\underset{1-1 onto}{⟶}{f}\left[\mathrm{\omega }\setminus \left\{\varnothing \right\}\right]\right)\to \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\approx {f}\left[\mathrm{\omega }\setminus \left\{\varnothing \right\}\right]$
31 25 29 30 sylancr ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\approx {f}\left[\mathrm{\omega }\setminus \left\{\varnothing \right\}\right]$
32 f1orn ${⊢}{f}:\mathrm{\omega }\underset{1-1 onto}{⟶}\mathrm{ran}{f}↔\left({f}Fn\mathrm{\omega }\wedge \mathrm{Fun}{{f}}^{-1}\right)$
33 32 simprbi ${⊢}{f}:\mathrm{\omega }\underset{1-1 onto}{⟶}\mathrm{ran}{f}\to \mathrm{Fun}{{f}}^{-1}$
34 imadif ${⊢}\mathrm{Fun}{{f}}^{-1}\to {f}\left[\mathrm{\omega }\setminus \left\{\varnothing \right\}\right]={f}\left[\mathrm{\omega }\right]\setminus {f}\left[\left\{\varnothing \right\}\right]$
35 16 33 34 3syl ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {f}\left[\mathrm{\omega }\setminus \left\{\varnothing \right\}\right]={f}\left[\mathrm{\omega }\right]\setminus {f}\left[\left\{\varnothing \right\}\right]$
36 f1fn ${⊢}{f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\to {f}Fn\mathrm{\omega }$
37 36 adantl ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {f}Fn\mathrm{\omega }$
38 fnima ${⊢}{f}Fn\mathrm{\omega }\to {f}\left[\mathrm{\omega }\right]=\mathrm{ran}{f}$
39 37 38 syl ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {f}\left[\mathrm{\omega }\right]=\mathrm{ran}{f}$
40 fnsnfv ${⊢}\left({f}Fn\mathrm{\omega }\wedge \varnothing \in \mathrm{\omega }\right)\to \left\{{f}\left(\varnothing \right)\right\}={f}\left[\left\{\varnothing \right\}\right]$
41 37 9 40 sylancl ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left\{{f}\left(\varnothing \right)\right\}={f}\left[\left\{\varnothing \right\}\right]$
42 41 eqcomd ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {f}\left[\left\{\varnothing \right\}\right]=\left\{{f}\left(\varnothing \right)\right\}$
43 39 42 difeq12d ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {f}\left[\mathrm{\omega }\right]\setminus {f}\left[\left\{\varnothing \right\}\right]=\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}$
44 35 43 eqtrd ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {f}\left[\mathrm{\omega }\setminus \left\{\varnothing \right\}\right]=\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}$
45 31 44 breqtrd ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\approx \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)$
46 entr ${⊢}\left(\mathrm{\omega }\approx \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\wedge \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\approx \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\right)\to \mathrm{\omega }\approx \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)$
47 24 45 46 syl2anc ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \mathrm{\omega }\approx \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)$
48 entr ${⊢}\left(\mathrm{ran}{f}\approx \mathrm{\omega }\wedge \mathrm{\omega }\approx \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\right)\to \mathrm{ran}{f}\approx \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)$
49 19 47 48 syl2anc ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \mathrm{ran}{f}\approx \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)$
50 difexg ${⊢}{A}\in \mathrm{V}\to {A}\setminus \mathrm{ran}{f}\in \mathrm{V}$
51 enrefg ${⊢}{A}\setminus \mathrm{ran}{f}\in \mathrm{V}\to \left({A}\setminus \mathrm{ran}{f}\right)\approx \left({A}\setminus \mathrm{ran}{f}\right)$
52 5 50 51 3syl ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left({A}\setminus \mathrm{ran}{f}\right)\approx \left({A}\setminus \mathrm{ran}{f}\right)$
53 disjdif ${⊢}\mathrm{ran}{f}\cap \left({A}\setminus \mathrm{ran}{f}\right)=\varnothing$
54 53 a1i ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \mathrm{ran}{f}\cap \left({A}\setminus \mathrm{ran}{f}\right)=\varnothing$
55 difss ${⊢}\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\subseteq \mathrm{ran}{f}$
56 ssrin ${⊢}\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\subseteq \mathrm{ran}{f}\to \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\cap \left({A}\setminus \mathrm{ran}{f}\right)\subseteq \mathrm{ran}{f}\cap \left({A}\setminus \mathrm{ran}{f}\right)$
57 55 56 ax-mp ${⊢}\left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\cap \left({A}\setminus \mathrm{ran}{f}\right)\subseteq \mathrm{ran}{f}\cap \left({A}\setminus \mathrm{ran}{f}\right)$
58 sseq0 ${⊢}\left(\left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\cap \left({A}\setminus \mathrm{ran}{f}\right)\subseteq \mathrm{ran}{f}\cap \left({A}\setminus \mathrm{ran}{f}\right)\wedge \mathrm{ran}{f}\cap \left({A}\setminus \mathrm{ran}{f}\right)=\varnothing \right)\to \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\cap \left({A}\setminus \mathrm{ran}{f}\right)=\varnothing$
59 57 53 58 mp2an ${⊢}\left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\cap \left({A}\setminus \mathrm{ran}{f}\right)=\varnothing$
60 59 a1i ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\cap \left({A}\setminus \mathrm{ran}{f}\right)=\varnothing$
61 unen ${⊢}\left(\left(\mathrm{ran}{f}\approx \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\wedge \left({A}\setminus \mathrm{ran}{f}\right)\approx \left({A}\setminus \mathrm{ran}{f}\right)\right)\wedge \left(\mathrm{ran}{f}\cap \left({A}\setminus \mathrm{ran}{f}\right)=\varnothing \wedge \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\cap \left({A}\setminus \mathrm{ran}{f}\right)=\varnothing \right)\right)\to \left(\mathrm{ran}{f}\cup \left({A}\setminus \mathrm{ran}{f}\right)\right)\approx \left(\left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\cup \left({A}\setminus \mathrm{ran}{f}\right)\right)$
62 49 52 54 60 61 syl22anc ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left(\mathrm{ran}{f}\cup \left({A}\setminus \mathrm{ran}{f}\right)\right)\approx \left(\left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\cup \left({A}\setminus \mathrm{ran}{f}\right)\right)$
63 8 frnd ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \mathrm{ran}{f}\subseteq {A}$
64 undif ${⊢}\mathrm{ran}{f}\subseteq {A}↔\mathrm{ran}{f}\cup \left({A}\setminus \mathrm{ran}{f}\right)={A}$
65 63 64 sylib ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \mathrm{ran}{f}\cup \left({A}\setminus \mathrm{ran}{f}\right)={A}$
66 uncom ${⊢}\left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\cup \left({A}\setminus \mathrm{ran}{f}\right)=\left({A}\setminus \mathrm{ran}{f}\right)\cup \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)$
67 eldifn ${⊢}{f}\left(\varnothing \right)\in \left({A}\setminus \mathrm{ran}{f}\right)\to ¬{f}\left(\varnothing \right)\in \mathrm{ran}{f}$
68 fnfvelrn ${⊢}\left({f}Fn\mathrm{\omega }\wedge \varnothing \in \mathrm{\omega }\right)\to {f}\left(\varnothing \right)\in \mathrm{ran}{f}$
69 37 9 68 sylancl ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {f}\left(\varnothing \right)\in \mathrm{ran}{f}$
70 67 69 nsyl3 ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to ¬{f}\left(\varnothing \right)\in \left({A}\setminus \mathrm{ran}{f}\right)$
71 disjsn ${⊢}\left({A}\setminus \mathrm{ran}{f}\right)\cap \left\{{f}\left(\varnothing \right)\right\}=\varnothing ↔¬{f}\left(\varnothing \right)\in \left({A}\setminus \mathrm{ran}{f}\right)$
72 70 71 sylibr ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left({A}\setminus \mathrm{ran}{f}\right)\cap \left\{{f}\left(\varnothing \right)\right\}=\varnothing$
73 undif4 ${⊢}\left({A}\setminus \mathrm{ran}{f}\right)\cap \left\{{f}\left(\varnothing \right)\right\}=\varnothing \to \left({A}\setminus \mathrm{ran}{f}\right)\cup \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)=\left(\left({A}\setminus \mathrm{ran}{f}\right)\cup \mathrm{ran}{f}\right)\setminus \left\{{f}\left(\varnothing \right)\right\}$
74 72 73 syl ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left({A}\setminus \mathrm{ran}{f}\right)\cup \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)=\left(\left({A}\setminus \mathrm{ran}{f}\right)\cup \mathrm{ran}{f}\right)\setminus \left\{{f}\left(\varnothing \right)\right\}$
75 uncom ${⊢}\left({A}\setminus \mathrm{ran}{f}\right)\cup \mathrm{ran}{f}=\mathrm{ran}{f}\cup \left({A}\setminus \mathrm{ran}{f}\right)$
76 75 65 syl5eq ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left({A}\setminus \mathrm{ran}{f}\right)\cup \mathrm{ran}{f}={A}$
77 76 difeq1d ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left(\left({A}\setminus \mathrm{ran}{f}\right)\cup \mathrm{ran}{f}\right)\setminus \left\{{f}\left(\varnothing \right)\right\}={A}\setminus \left\{{f}\left(\varnothing \right)\right\}$
78 74 77 eqtrd ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left({A}\setminus \mathrm{ran}{f}\right)\cup \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)={A}\setminus \left\{{f}\left(\varnothing \right)\right\}$
79 66 78 syl5eq ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left(\mathrm{ran}{f}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\cup \left({A}\setminus \mathrm{ran}{f}\right)={A}\setminus \left\{{f}\left(\varnothing \right)\right\}$
80 62 65 79 3brtr3d ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to {A}\approx \left({A}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)$
81 80 ensymd ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left({A}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\approx {A}$
82 entr ${⊢}\left(\left({A}\setminus \left\{{B}\right\}\right)\approx \left({A}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\wedge \left({A}\setminus \left\{{f}\left(\varnothing \right)\right\}\right)\approx {A}\right)\to \left({A}\setminus \left\{{B}\right\}\right)\approx {A}$
83 13 81 82 syl2anc ${⊢}\left(\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\wedge {f}:\mathrm{\omega }\underset{1-1}{⟶}{A}\right)\to \left({A}\setminus \left\{{B}\right\}\right)\approx {A}$
84 2 83 exlimddv ${⊢}\left(\mathrm{\omega }\preccurlyeq {A}\wedge {B}\in {A}\right)\to \left({A}\setminus \left\{{B}\right\}\right)\approx {A}$
85 difsn ${⊢}¬{B}\in {A}\to {A}\setminus \left\{{B}\right\}={A}$
86 85 adantl ${⊢}\left(\mathrm{\omega }\preccurlyeq {A}\wedge ¬{B}\in {A}\right)\to {A}\setminus \left\{{B}\right\}={A}$
87 enrefg ${⊢}{A}\in \mathrm{V}\to {A}\approx {A}$
88 4 87 syl ${⊢}\mathrm{\omega }\preccurlyeq {A}\to {A}\approx {A}$
89 88 adantr ${⊢}\left(\mathrm{\omega }\preccurlyeq {A}\wedge ¬{B}\in {A}\right)\to {A}\approx {A}$
90 86 89 eqbrtrd ${⊢}\left(\mathrm{\omega }\preccurlyeq {A}\wedge ¬{B}\in {A}\right)\to \left({A}\setminus \left\{{B}\right\}\right)\approx {A}$
91 84 90 pm2.61dan ${⊢}\mathrm{\omega }\preccurlyeq {A}\to \left({A}\setminus \left\{{B}\right\}\right)\approx {A}$