# Metamath Proof Explorer

## Theorem ackbij1lem18

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Hypothesis ackbij.f ${⊢}{F}=\left({x}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{{y}\in {x}}\left(\left\{{y}\right\}×𝒫{y}\right)\right)\right)$
Assertion ackbij1lem18 ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \exists {b}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{F}\left({b}\right)=\mathrm{suc}{F}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 ackbij.f ${⊢}{F}=\left({x}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{{y}\in {x}}\left(\left\{{y}\right\}×𝒫{y}\right)\right)\right)$
2 difss ${⊢}{A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\subseteq {A}$
3 1 ackbij1lem11 ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\subseteq {A}\right)\to {A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
4 2 3 mpan2 ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
5 difss ${⊢}\mathrm{\omega }\setminus {A}\subseteq \mathrm{\omega }$
6 omsson ${⊢}\mathrm{\omega }\subseteq \mathrm{On}$
7 5 6 sstri ${⊢}\mathrm{\omega }\setminus {A}\subseteq \mathrm{On}$
8 ominf ${⊢}¬\mathrm{\omega }\in \mathrm{Fin}$
9 elinel2 ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {A}\in \mathrm{Fin}$
10 difinf ${⊢}\left(¬\mathrm{\omega }\in \mathrm{Fin}\wedge {A}\in \mathrm{Fin}\right)\to ¬\mathrm{\omega }\setminus {A}\in \mathrm{Fin}$
11 8 9 10 sylancr ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to ¬\mathrm{\omega }\setminus {A}\in \mathrm{Fin}$
12 0fin ${⊢}\varnothing \in \mathrm{Fin}$
13 eleq1 ${⊢}\mathrm{\omega }\setminus {A}=\varnothing \to \left(\mathrm{\omega }\setminus {A}\in \mathrm{Fin}↔\varnothing \in \mathrm{Fin}\right)$
14 12 13 mpbiri ${⊢}\mathrm{\omega }\setminus {A}=\varnothing \to \mathrm{\omega }\setminus {A}\in \mathrm{Fin}$
15 14 necon3bi ${⊢}¬\mathrm{\omega }\setminus {A}\in \mathrm{Fin}\to \mathrm{\omega }\setminus {A}\ne \varnothing$
16 11 15 syl ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \mathrm{\omega }\setminus {A}\ne \varnothing$
17 onint ${⊢}\left(\mathrm{\omega }\setminus {A}\subseteq \mathrm{On}\wedge \mathrm{\omega }\setminus {A}\ne \varnothing \right)\to \bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \left(\mathrm{\omega }\setminus {A}\right)$
18 7 16 17 sylancr ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \left(\mathrm{\omega }\setminus {A}\right)$
19 18 eldifad ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \mathrm{\omega }$
20 ackbij1lem4 ${⊢}\bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \mathrm{\omega }\to \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
21 19 20 syl ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
22 ackbij1lem6 ${⊢}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
23 4 21 22 syl2anc ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
24 18 eldifbd ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to ¬\bigcap \left(\mathrm{\omega }\setminus {A}\right)\in {A}$
25 disjsn ${⊢}{A}\cap \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}=\varnothing ↔¬\bigcap \left(\mathrm{\omega }\setminus {A}\right)\in {A}$
26 24 25 sylibr ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {A}\cap \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}=\varnothing$
27 ssdisj ${⊢}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\subseteq {A}\wedge {A}\cap \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}=\varnothing \right)\to \left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cap \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}=\varnothing$
28 2 26 27 sylancr ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cap \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}=\varnothing$
29 1 ackbij1lem9 ${⊢}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge \left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cap \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}=\varnothing \right)\to {F}\left(\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\right)={F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}{F}\left(\left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\right)$
30 4 21 28 29 syl3anc ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left(\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\right)={F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}{F}\left(\left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\right)$
31 1 ackbij1lem14 ${⊢}\bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \mathrm{\omega }\to {F}\left(\left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\right)=\mathrm{suc}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)$
32 19 31 syl ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left(\left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\right)=\mathrm{suc}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)$
33 32 oveq2d ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}{F}\left(\left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\right)={F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}\mathrm{suc}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)$
34 1 ackbij1lem10 ${⊢}{F}:𝒫\mathrm{\omega }\cap \mathrm{Fin}⟶\mathrm{\omega }$
35 34 ffvelrni ${⊢}{A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\in \mathrm{\omega }$
36 4 35 syl ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\in \mathrm{\omega }$
37 ackbij1lem3 ${⊢}\bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \mathrm{\omega }\to \bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
38 19 37 syl ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
39 34 ffvelrni ${⊢}\bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\in \mathrm{\omega }$
40 38 39 syl ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\in \mathrm{\omega }$
41 nnasuc ${⊢}\left({F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\in \mathrm{\omega }\wedge {F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\in \mathrm{\omega }\right)\to {F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}\mathrm{suc}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)=\mathrm{suc}\left({F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\right)$
42 36 40 41 syl2anc ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}\mathrm{suc}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)=\mathrm{suc}\left({F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\right)$
43 incom ${⊢}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cap \bigcap \left(\mathrm{\omega }\setminus {A}\right)=\bigcap \left(\mathrm{\omega }\setminus {A}\right)\cap \left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)$
44 disjdif ${⊢}\bigcap \left(\mathrm{\omega }\setminus {A}\right)\cap \left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)=\varnothing$
45 43 44 eqtri ${⊢}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cap \bigcap \left(\mathrm{\omega }\setminus {A}\right)=\varnothing$
46 45 a1i ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cap \bigcap \left(\mathrm{\omega }\setminus {A}\right)=\varnothing$
47 1 ackbij1lem9 ${⊢}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge \bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge \left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cap \bigcap \left(\mathrm{\omega }\setminus {A}\right)=\varnothing \right)\to {F}\left(\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)={F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)$
48 4 38 46 47 syl3anc ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left(\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)={F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)$
49 uncom ${⊢}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \bigcap \left(\mathrm{\omega }\setminus {A}\right)=\bigcap \left(\mathrm{\omega }\setminus {A}\right)\cup \left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)$
50 onnmin ${⊢}\left(\mathrm{\omega }\setminus {A}\subseteq \mathrm{On}\wedge {a}\in \left(\mathrm{\omega }\setminus {A}\right)\right)\to ¬{a}\in \bigcap \left(\mathrm{\omega }\setminus {A}\right)$
51 7 50 mpan ${⊢}{a}\in \left(\mathrm{\omega }\setminus {A}\right)\to ¬{a}\in \bigcap \left(\mathrm{\omega }\setminus {A}\right)$
52 51 con2i ${⊢}{a}\in \bigcap \left(\mathrm{\omega }\setminus {A}\right)\to ¬{a}\in \left(\mathrm{\omega }\setminus {A}\right)$
53 52 adantl ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {a}\in \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\to ¬{a}\in \left(\mathrm{\omega }\setminus {A}\right)$
54 ordom ${⊢}\mathrm{Ord}\mathrm{\omega }$
55 ordelss ${⊢}\left(\mathrm{Ord}\mathrm{\omega }\wedge \bigcap \left(\mathrm{\omega }\setminus {A}\right)\in \mathrm{\omega }\right)\to \bigcap \left(\mathrm{\omega }\setminus {A}\right)\subseteq \mathrm{\omega }$
56 54 19 55 sylancr ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \bigcap \left(\mathrm{\omega }\setminus {A}\right)\subseteq \mathrm{\omega }$
57 56 sselda ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {a}\in \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\to {a}\in \mathrm{\omega }$
58 eldif ${⊢}{a}\in \left(\mathrm{\omega }\setminus {A}\right)↔\left({a}\in \mathrm{\omega }\wedge ¬{a}\in {A}\right)$
59 58 simplbi2 ${⊢}{a}\in \mathrm{\omega }\to \left(¬{a}\in {A}\to {a}\in \left(\mathrm{\omega }\setminus {A}\right)\right)$
60 59 orrd ${⊢}{a}\in \mathrm{\omega }\to \left({a}\in {A}\vee {a}\in \left(\mathrm{\omega }\setminus {A}\right)\right)$
61 60 orcomd ${⊢}{a}\in \mathrm{\omega }\to \left({a}\in \left(\mathrm{\omega }\setminus {A}\right)\vee {a}\in {A}\right)$
62 57 61 syl ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {a}\in \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\to \left({a}\in \left(\mathrm{\omega }\setminus {A}\right)\vee {a}\in {A}\right)$
63 orel1 ${⊢}¬{a}\in \left(\mathrm{\omega }\setminus {A}\right)\to \left(\left({a}\in \left(\mathrm{\omega }\setminus {A}\right)\vee {a}\in {A}\right)\to {a}\in {A}\right)$
64 53 62 63 sylc ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {a}\in \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\to {a}\in {A}$
65 64 ex ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \left({a}\in \bigcap \left(\mathrm{\omega }\setminus {A}\right)\to {a}\in {A}\right)$
66 65 ssrdv ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \bigcap \left(\mathrm{\omega }\setminus {A}\right)\subseteq {A}$
67 undif ${⊢}\bigcap \left(\mathrm{\omega }\setminus {A}\right)\subseteq {A}↔\bigcap \left(\mathrm{\omega }\setminus {A}\right)\cup \left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)={A}$
68 66 67 sylib ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \bigcap \left(\mathrm{\omega }\setminus {A}\right)\cup \left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)={A}$
69 49 68 syl5eq ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \bigcap \left(\mathrm{\omega }\setminus {A}\right)={A}$
70 69 fveq2d ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left(\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)={F}\left({A}\right)$
71 48 70 eqtr3d ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)={F}\left({A}\right)$
72 suceq ${⊢}{F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)={F}\left({A}\right)\to \mathrm{suc}\left({F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\right)=\mathrm{suc}{F}\left({A}\right)$
73 71 72 syl ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \mathrm{suc}\left({F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\right)=\mathrm{suc}{F}\left({A}\right)$
74 42 73 eqtrd ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right){+}_{𝑜}\mathrm{suc}{F}\left(\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)=\mathrm{suc}{F}\left({A}\right)$
75 30 33 74 3eqtrd ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left(\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\right)=\mathrm{suc}{F}\left({A}\right)$
76 fveqeq2 ${⊢}{b}=\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\to \left({F}\left({b}\right)=\mathrm{suc}{F}\left({A}\right)↔{F}\left(\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\right)=\mathrm{suc}{F}\left({A}\right)\right)$
77 76 rspcev ${⊢}\left(\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {F}\left(\left({A}\setminus \bigcap \left(\mathrm{\omega }\setminus {A}\right)\right)\cup \left\{\bigcap \left(\mathrm{\omega }\setminus {A}\right)\right\}\right)=\mathrm{suc}{F}\left({A}\right)\right)\to \exists {b}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{F}\left({b}\right)=\mathrm{suc}{F}\left({A}\right)$
78 23 75 77 syl2anc ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \exists {b}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{F}\left({b}\right)=\mathrm{suc}{F}\left({A}\right)$