# Metamath Proof Explorer

## Theorem ackbij1lem16

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 ackbij1lem16 ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\right)={F}\left({B}\right)\to {A}={B}\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 inss1 ${⊢}𝒫\mathrm{\omega }\cap \mathrm{Fin}\subseteq 𝒫\mathrm{\omega }$
3 2 sseli ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {A}\in 𝒫\mathrm{\omega }$
4 3 elpwid ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {A}\subseteq \mathrm{\omega }$
5 4 adantr ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to {A}\subseteq \mathrm{\omega }$
6 2 sseli ${⊢}{B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {B}\in 𝒫\mathrm{\omega }$
7 6 elpwid ${⊢}{B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {B}\subseteq \mathrm{\omega }$
8 7 adantl ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to {B}\subseteq \mathrm{\omega }$
9 5 8 unssd ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to {A}\cup {B}\subseteq \mathrm{\omega }$
10 inss2 ${⊢}𝒫\mathrm{\omega }\cap \mathrm{Fin}\subseteq \mathrm{Fin}$
11 10 sseli ${⊢}{A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {A}\in \mathrm{Fin}$
12 10 sseli ${⊢}{B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {B}\in \mathrm{Fin}$
13 unfi ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to {A}\cup {B}\in \mathrm{Fin}$
14 11 12 13 syl2an ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to {A}\cup {B}\in \mathrm{Fin}$
15 nnunifi ${⊢}\left({A}\cup {B}\subseteq \mathrm{\omega }\wedge {A}\cup {B}\in \mathrm{Fin}\right)\to \bigcup \left({A}\cup {B}\right)\in \mathrm{\omega }$
16 9 14 15 syl2anc ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \bigcup \left({A}\cup {B}\right)\in \mathrm{\omega }$
17 peano2 ${⊢}\bigcup \left({A}\cup {B}\right)\in \mathrm{\omega }\to \mathrm{suc}\bigcup \left({A}\cup {B}\right)\in \mathrm{\omega }$
18 16 17 syl ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \mathrm{suc}\bigcup \left({A}\cup {B}\right)\in \mathrm{\omega }$
19 ineq2 ${⊢}{a}=\varnothing \to {A}\cap {a}={A}\cap \varnothing$
20 19 fveq2d ${⊢}{a}=\varnothing \to {F}\left({A}\cap {a}\right)={F}\left({A}\cap \varnothing \right)$
21 ineq2 ${⊢}{a}=\varnothing \to {B}\cap {a}={B}\cap \varnothing$
22 21 fveq2d ${⊢}{a}=\varnothing \to {F}\left({B}\cap {a}\right)={F}\left({B}\cap \varnothing \right)$
23 20 22 eqeq12d ${⊢}{a}=\varnothing \to \left({F}\left({A}\cap {a}\right)={F}\left({B}\cap {a}\right)↔{F}\left({A}\cap \varnothing \right)={F}\left({B}\cap \varnothing \right)\right)$
24 19 21 eqeq12d ${⊢}{a}=\varnothing \to \left({A}\cap {a}={B}\cap {a}↔{A}\cap \varnothing ={B}\cap \varnothing \right)$
25 23 24 imbi12d ${⊢}{a}=\varnothing \to \left(\left({F}\left({A}\cap {a}\right)={F}\left({B}\cap {a}\right)\to {A}\cap {a}={B}\cap {a}\right)↔\left({F}\left({A}\cap \varnothing \right)={F}\left({B}\cap \varnothing \right)\to {A}\cap \varnothing ={B}\cap \varnothing \right)\right)$
26 25 imbi2d ${⊢}{a}=\varnothing \to \left(\left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap {a}\right)={F}\left({B}\cap {a}\right)\to {A}\cap {a}={B}\cap {a}\right)\right)↔\left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap \varnothing \right)={F}\left({B}\cap \varnothing \right)\to {A}\cap \varnothing ={B}\cap \varnothing \right)\right)\right)$
27 ineq2 ${⊢}{a}={b}\to {A}\cap {a}={A}\cap {b}$
28 27 fveq2d ${⊢}{a}={b}\to {F}\left({A}\cap {a}\right)={F}\left({A}\cap {b}\right)$
29 ineq2 ${⊢}{a}={b}\to {B}\cap {a}={B}\cap {b}$
30 29 fveq2d ${⊢}{a}={b}\to {F}\left({B}\cap {a}\right)={F}\left({B}\cap {b}\right)$
31 28 30 eqeq12d ${⊢}{a}={b}\to \left({F}\left({A}\cap {a}\right)={F}\left({B}\cap {a}\right)↔{F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\right)$
32 27 29 eqeq12d ${⊢}{a}={b}\to \left({A}\cap {a}={B}\cap {a}↔{A}\cap {b}={B}\cap {b}\right)$
33 31 32 imbi12d ${⊢}{a}={b}\to \left(\left({F}\left({A}\cap {a}\right)={F}\left({B}\cap {a}\right)\to {A}\cap {a}={B}\cap {a}\right)↔\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\right)$
34 33 imbi2d ${⊢}{a}={b}\to \left(\left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap {a}\right)={F}\left({B}\cap {a}\right)\to {A}\cap {a}={B}\cap {a}\right)\right)↔\left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\right)\right)$
35 ineq2 ${⊢}{a}=\mathrm{suc}{b}\to {A}\cap {a}={A}\cap \mathrm{suc}{b}$
36 35 fveq2d ${⊢}{a}=\mathrm{suc}{b}\to {F}\left({A}\cap {a}\right)={F}\left({A}\cap \mathrm{suc}{b}\right)$
37 ineq2 ${⊢}{a}=\mathrm{suc}{b}\to {B}\cap {a}={B}\cap \mathrm{suc}{b}$
38 37 fveq2d ${⊢}{a}=\mathrm{suc}{b}\to {F}\left({B}\cap {a}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)$
39 36 38 eqeq12d ${⊢}{a}=\mathrm{suc}{b}\to \left({F}\left({A}\cap {a}\right)={F}\left({B}\cap {a}\right)↔{F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)$
40 35 37 eqeq12d ${⊢}{a}=\mathrm{suc}{b}\to \left({A}\cap {a}={B}\cap {a}↔{A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)$
41 39 40 imbi12d ${⊢}{a}=\mathrm{suc}{b}\to \left(\left({F}\left({A}\cap {a}\right)={F}\left({B}\cap {a}\right)\to {A}\cap {a}={B}\cap {a}\right)↔\left({F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)\right)$
42 41 imbi2d ${⊢}{a}=\mathrm{suc}{b}\to \left(\left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap {a}\right)={F}\left({B}\cap {a}\right)\to {A}\cap {a}={B}\cap {a}\right)\right)↔\left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)\right)\right)$
43 ineq2 ${⊢}{a}=\mathrm{suc}\bigcup \left({A}\cup {B}\right)\to {A}\cap {a}={A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)$
44 43 fveq2d ${⊢}{a}=\mathrm{suc}\bigcup \left({A}\cup {B}\right)\to {F}\left({A}\cap {a}\right)={F}\left({A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)$
45 ineq2 ${⊢}{a}=\mathrm{suc}\bigcup \left({A}\cup {B}\right)\to {B}\cap {a}={B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)$
46 45 fveq2d ${⊢}{a}=\mathrm{suc}\bigcup \left({A}\cup {B}\right)\to {F}\left({B}\cap {a}\right)={F}\left({B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)$
47 44 46 eqeq12d ${⊢}{a}=\mathrm{suc}\bigcup \left({A}\cup {B}\right)\to \left({F}\left({A}\cap {a}\right)={F}\left({B}\cap {a}\right)↔{F}\left({A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)={F}\left({B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)\right)$
48 43 45 eqeq12d ${⊢}{a}=\mathrm{suc}\bigcup \left({A}\cup {B}\right)\to \left({A}\cap {a}={B}\cap {a}↔{A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)={B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)$
49 47 48 imbi12d ${⊢}{a}=\mathrm{suc}\bigcup \left({A}\cup {B}\right)\to \left(\left({F}\left({A}\cap {a}\right)={F}\left({B}\cap {a}\right)\to {A}\cap {a}={B}\cap {a}\right)↔\left({F}\left({A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)={F}\left({B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)\to {A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)={B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)\right)$
50 49 imbi2d ${⊢}{a}=\mathrm{suc}\bigcup \left({A}\cup {B}\right)\to \left(\left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap {a}\right)={F}\left({B}\cap {a}\right)\to {A}\cap {a}={B}\cap {a}\right)\right)↔\left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)={F}\left({B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)\to {A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)={B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)\right)\right)$
51 in0 ${⊢}{A}\cap \varnothing =\varnothing$
52 in0 ${⊢}{B}\cap \varnothing =\varnothing$
53 51 52 eqtr4i ${⊢}{A}\cap \varnothing ={B}\cap \varnothing$
54 53 2a1i ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap \varnothing \right)={F}\left({B}\cap \varnothing \right)\to {A}\cap \varnothing ={B}\cap \varnothing \right)$
55 simp13 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)$
56 3simpa ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\to \left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)$
57 ackbij1lem2 ${⊢}{b}\in {A}\to {A}\cap \mathrm{suc}{b}=\left\{{b}\right\}\cup \left({A}\cap {b}\right)$
58 57 fveq2d ${⊢}{b}\in {A}\to {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left(\left\{{b}\right\}\cup \left({A}\cap {b}\right)\right)$
59 58 3ad2ant2 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left(\left\{{b}\right\}\cup \left({A}\cap {b}\right)\right)$
60 ackbij1lem4 ${⊢}{b}\in \mathrm{\omega }\to \left\{{b}\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
61 60 adantr ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to \left\{{b}\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
62 simprl ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to {A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
63 inss1 ${⊢}{A}\cap {b}\subseteq {A}$
64 1 ackbij1lem11 ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {A}\cap {b}\subseteq {A}\right)\to {A}\cap {b}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
65 62 63 64 sylancl ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to {A}\cap {b}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
66 incom ${⊢}\left\{{b}\right\}\cap \left({A}\cap {b}\right)=\left({A}\cap {b}\right)\cap \left\{{b}\right\}$
67 inss2 ${⊢}{A}\cap {b}\subseteq {b}$
68 nnord ${⊢}{b}\in \mathrm{\omega }\to \mathrm{Ord}{b}$
69 orddisj ${⊢}\mathrm{Ord}{b}\to {b}\cap \left\{{b}\right\}=\varnothing$
70 68 69 syl ${⊢}{b}\in \mathrm{\omega }\to {b}\cap \left\{{b}\right\}=\varnothing$
71 70 adantr ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to {b}\cap \left\{{b}\right\}=\varnothing$
72 ssdisj ${⊢}\left({A}\cap {b}\subseteq {b}\wedge {b}\cap \left\{{b}\right\}=\varnothing \right)\to \left({A}\cap {b}\right)\cap \left\{{b}\right\}=\varnothing$
73 67 71 72 sylancr ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to \left({A}\cap {b}\right)\cap \left\{{b}\right\}=\varnothing$
74 66 73 syl5eq ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to \left\{{b}\right\}\cap \left({A}\cap {b}\right)=\varnothing$
75 1 ackbij1lem9 ${⊢}\left(\left\{{b}\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {A}\cap {b}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge \left\{{b}\right\}\cap \left({A}\cap {b}\right)=\varnothing \right)\to {F}\left(\left\{{b}\right\}\cup \left({A}\cap {b}\right)\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({A}\cap {b}\right)$
76 61 65 74 75 syl3anc ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to {F}\left(\left\{{b}\right\}\cup \left({A}\cap {b}\right)\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({A}\cap {b}\right)$
77 76 3ad2ant1 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to {F}\left(\left\{{b}\right\}\cup \left({A}\cap {b}\right)\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({A}\cap {b}\right)$
78 59 77 eqtrd ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({A}\cap {b}\right)$
79 56 78 syl3an1 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({A}\cap {b}\right)$
80 ackbij1lem2 ${⊢}{b}\in {B}\to {B}\cap \mathrm{suc}{b}=\left\{{b}\right\}\cup \left({B}\cap {b}\right)$
81 80 fveq2d ${⊢}{b}\in {B}\to {F}\left({B}\cap \mathrm{suc}{b}\right)={F}\left(\left\{{b}\right\}\cup \left({B}\cap {b}\right)\right)$
82 81 3ad2ant3 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to {F}\left({B}\cap \mathrm{suc}{b}\right)={F}\left(\left\{{b}\right\}\cup \left({B}\cap {b}\right)\right)$
83 simprr ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
84 inss1 ${⊢}{B}\cap {b}\subseteq {B}$
85 1 ackbij1lem11 ${⊢}\left({B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\cap {b}\subseteq {B}\right)\to {B}\cap {b}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
86 83 84 85 sylancl ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to {B}\cap {b}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
87 incom ${⊢}\left\{{b}\right\}\cap \left({B}\cap {b}\right)=\left({B}\cap {b}\right)\cap \left\{{b}\right\}$
88 inss2 ${⊢}{B}\cap {b}\subseteq {b}$
89 ssdisj ${⊢}\left({B}\cap {b}\subseteq {b}\wedge {b}\cap \left\{{b}\right\}=\varnothing \right)\to \left({B}\cap {b}\right)\cap \left\{{b}\right\}=\varnothing$
90 88 71 89 sylancr ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to \left({B}\cap {b}\right)\cap \left\{{b}\right\}=\varnothing$
91 87 90 syl5eq ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to \left\{{b}\right\}\cap \left({B}\cap {b}\right)=\varnothing$
92 1 ackbij1lem9 ${⊢}\left(\left\{{b}\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\cap {b}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge \left\{{b}\right\}\cap \left({B}\cap {b}\right)=\varnothing \right)\to {F}\left(\left\{{b}\right\}\cup \left({B}\cap {b}\right)\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({B}\cap {b}\right)$
93 61 86 91 92 syl3anc ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to {F}\left(\left\{{b}\right\}\cup \left({B}\cap {b}\right)\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({B}\cap {b}\right)$
94 93 3ad2ant1 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to {F}\left(\left\{{b}\right\}\cup \left({B}\cap {b}\right)\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({B}\cap {b}\right)$
95 82 94 eqtrd ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to {F}\left({B}\cap \mathrm{suc}{b}\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({B}\cap {b}\right)$
96 56 95 syl3an1 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to {F}\left({B}\cap \mathrm{suc}{b}\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({B}\cap {b}\right)$
97 55 79 96 3eqtr3d ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to {F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({A}\cap {b}\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({B}\cap {b}\right)$
98 1 ackbij1lem10 ${⊢}{F}:𝒫\mathrm{\omega }\cap \mathrm{Fin}⟶\mathrm{\omega }$
99 98 ffvelrni ${⊢}\left\{{b}\right\}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left(\left\{{b}\right\}\right)\in \mathrm{\omega }$
100 61 99 syl ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to {F}\left(\left\{{b}\right\}\right)\in \mathrm{\omega }$
101 98 ffvelrni ${⊢}{A}\cap {b}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left({A}\cap {b}\right)\in \mathrm{\omega }$
102 65 101 syl ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to {F}\left({A}\cap {b}\right)\in \mathrm{\omega }$
103 98 ffvelrni ${⊢}{B}\cap {b}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to {F}\left({B}\cap {b}\right)\in \mathrm{\omega }$
104 86 103 syl ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to {F}\left({B}\cap {b}\right)\in \mathrm{\omega }$
105 nnacan ${⊢}\left({F}\left(\left\{{b}\right\}\right)\in \mathrm{\omega }\wedge {F}\left({A}\cap {b}\right)\in \mathrm{\omega }\wedge {F}\left({B}\cap {b}\right)\in \mathrm{\omega }\right)\to \left({F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({A}\cap {b}\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({B}\cap {b}\right)↔{F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\right)$
106 100 102 104 105 syl3anc ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\right)\to \left({F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({A}\cap {b}\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({B}\cap {b}\right)↔{F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\right)$
107 106 3adant3 ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\to \left({F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({A}\cap {b}\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({B}\cap {b}\right)↔{F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\right)$
108 107 3ad2ant1 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to \left({F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({A}\cap {b}\right)={F}\left(\left\{{b}\right\}\right){+}_{𝑜}{F}\left({B}\cap {b}\right)↔{F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\right)$
109 97 108 mpbid ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to {F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)$
110 uneq2 ${⊢}{A}\cap {b}={B}\cap {b}\to \left\{{b}\right\}\cup \left({A}\cap {b}\right)=\left\{{b}\right\}\cup \left({B}\cap {b}\right)$
111 110 adantl ${⊢}\left(\left({b}\in {A}\wedge {b}\in {B}\right)\wedge {A}\cap {b}={B}\cap {b}\right)\to \left\{{b}\right\}\cup \left({A}\cap {b}\right)=\left\{{b}\right\}\cup \left({B}\cap {b}\right)$
112 57 ad2antrr ${⊢}\left(\left({b}\in {A}\wedge {b}\in {B}\right)\wedge {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}=\left\{{b}\right\}\cup \left({A}\cap {b}\right)$
113 80 ad2antlr ${⊢}\left(\left({b}\in {A}\wedge {b}\in {B}\right)\wedge {A}\cap {b}={B}\cap {b}\right)\to {B}\cap \mathrm{suc}{b}=\left\{{b}\right\}\cup \left({B}\cap {b}\right)$
114 111 112 113 3eqtr4d ${⊢}\left(\left({b}\in {A}\wedge {b}\in {B}\right)\wedge {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}$
115 114 ex ${⊢}\left({b}\in {A}\wedge {b}\in {B}\right)\to \left({A}\cap {b}={B}\cap {b}\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)$
116 115 3adant1 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to \left({A}\cap {b}={B}\cap {b}\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)$
117 109 116 embantd ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge {b}\in {B}\right)\to \left(\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)$
118 117 3exp ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\to \left({b}\in {A}\to \left({b}\in {B}\to \left(\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)\right)\right)$
119 simp13 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge {b}\in {B}\right)\to {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)$
120 119 eqcomd ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge {b}\in {B}\right)\to {F}\left({B}\cap \mathrm{suc}{b}\right)={F}\left({A}\cap \mathrm{suc}{b}\right)$
121 simp12r ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge {b}\in {B}\right)\to {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
122 simp12l ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge {b}\in {B}\right)\to {A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
123 simp11 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge {b}\in {B}\right)\to {b}\in \mathrm{\omega }$
124 simp3 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge {b}\in {B}\right)\to {b}\in {B}$
125 simp2 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge {b}\in {B}\right)\to ¬{b}\in {A}$
126 1 ackbij1lem15 ${⊢}\left(\left({B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge \left({b}\in \mathrm{\omega }\wedge {b}\in {B}\wedge ¬{b}\in {A}\right)\right)\to ¬{F}\left({B}\cap \mathrm{suc}{b}\right)={F}\left({A}\cap \mathrm{suc}{b}\right)$
127 121 122 123 124 125 126 syl23anc ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge {b}\in {B}\right)\to ¬{F}\left({B}\cap \mathrm{suc}{b}\right)={F}\left({A}\cap \mathrm{suc}{b}\right)$
128 120 127 pm2.21dd ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge {b}\in {B}\right)\to \left(\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)$
129 128 3exp ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\to \left(¬{b}\in {A}\to \left({b}\in {B}\to \left(\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)\right)\right)$
130 118 129 pm2.61d ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\to \left({b}\in {B}\to \left(\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)\right)$
131 simp13 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge ¬{b}\in {B}\right)\to {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)$
132 simp12l ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge ¬{b}\in {B}\right)\to {A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
133 simp12r ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge ¬{b}\in {B}\right)\to {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$
134 simp11 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge ¬{b}\in {B}\right)\to {b}\in \mathrm{\omega }$
135 simp2 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge ¬{b}\in {B}\right)\to {b}\in {A}$
136 simp3 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge ¬{b}\in {B}\right)\to ¬{b}\in {B}$
137 1 ackbij1lem15 ${⊢}\left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge \left({b}\in \mathrm{\omega }\wedge {b}\in {A}\wedge ¬{b}\in {B}\right)\right)\to ¬{F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)$
138 132 133 134 135 136 137 syl23anc ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge ¬{b}\in {B}\right)\to ¬{F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)$
139 131 138 pm2.21dd ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge {b}\in {A}\wedge ¬{b}\in {B}\right)\to \left(\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)$
140 139 3exp ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\to \left({b}\in {A}\to \left(¬{b}\in {B}\to \left(\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)\right)\right)$
141 simp13 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge ¬{b}\in {B}\right)\to {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)$
142 ackbij1lem1 ${⊢}¬{b}\in {A}\to {A}\cap \mathrm{suc}{b}={A}\cap {b}$
143 142 adantr ${⊢}\left(¬{b}\in {A}\wedge ¬{b}\in {B}\right)\to {A}\cap \mathrm{suc}{b}={A}\cap {b}$
144 143 fveq2d ${⊢}\left(¬{b}\in {A}\wedge ¬{b}\in {B}\right)\to {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({A}\cap {b}\right)$
145 ackbij1lem1 ${⊢}¬{b}\in {B}\to {B}\cap \mathrm{suc}{b}={B}\cap {b}$
146 145 adantl ${⊢}\left(¬{b}\in {A}\wedge ¬{b}\in {B}\right)\to {B}\cap \mathrm{suc}{b}={B}\cap {b}$
147 146 fveq2d ${⊢}\left(¬{b}\in {A}\wedge ¬{b}\in {B}\right)\to {F}\left({B}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap {b}\right)$
148 144 147 eqeq12d ${⊢}\left(¬{b}\in {A}\wedge ¬{b}\in {B}\right)\to \left({F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)↔{F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\right)$
149 148 biimpd ${⊢}\left(¬{b}\in {A}\wedge ¬{b}\in {B}\right)\to \left({F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\to {F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\right)$
150 149 3adant1 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge ¬{b}\in {B}\right)\to \left({F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\to {F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\right)$
151 141 150 mpd ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge ¬{b}\in {B}\right)\to {F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)$
152 143 146 eqeq12d ${⊢}\left(¬{b}\in {A}\wedge ¬{b}\in {B}\right)\to \left({A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}↔{A}\cap {b}={B}\cap {b}\right)$
153 152 biimprd ${⊢}\left(¬{b}\in {A}\wedge ¬{b}\in {B}\right)\to \left({A}\cap {b}={B}\cap {b}\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)$
154 153 3adant1 ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge ¬{b}\in {B}\right)\to \left({A}\cap {b}={B}\cap {b}\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)$
155 151 154 embantd ${⊢}\left(\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\wedge ¬{b}\in {A}\wedge ¬{b}\in {B}\right)\to \left(\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)$
156 155 3exp ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\to \left(¬{b}\in {A}\to \left(¬{b}\in {B}\to \left(\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)\right)\right)$
157 140 156 pm2.61d ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\to \left(¬{b}\in {B}\to \left(\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)\right)$
158 130 157 pm2.61d ${⊢}\left({b}\in \mathrm{\omega }\wedge \left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\wedge {F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\right)\to \left(\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)$
159 158 3exp ${⊢}{b}\in \mathrm{\omega }\to \left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\to \left(\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)\right)\right)$
160 159 com34 ${⊢}{b}\in \mathrm{\omega }\to \left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left(\left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\to \left({F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)\right)\right)$
161 160 a2d ${⊢}{b}\in \mathrm{\omega }\to \left(\left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap {b}\right)={F}\left({B}\cap {b}\right)\to {A}\cap {b}={B}\cap {b}\right)\right)\to \left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap \mathrm{suc}{b}\right)={F}\left({B}\cap \mathrm{suc}{b}\right)\to {A}\cap \mathrm{suc}{b}={B}\cap \mathrm{suc}{b}\right)\right)\right)$
162 26 34 42 50 54 161 finds ${⊢}\mathrm{suc}\bigcup \left({A}\cup {B}\right)\in \mathrm{\omega }\to \left(\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)={F}\left({B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)\to {A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)={B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)\right)$
163 18 162 mpcom ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)={F}\left({B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)\to {A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)={B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)$
164 omsson ${⊢}\mathrm{\omega }\subseteq \mathrm{On}$
165 9 164 sstrdi ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to {A}\cup {B}\subseteq \mathrm{On}$
166 onsucuni ${⊢}{A}\cup {B}\subseteq \mathrm{On}\to {A}\cup {B}\subseteq \mathrm{suc}\bigcup \left({A}\cup {B}\right)$
167 165 166 syl ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to {A}\cup {B}\subseteq \mathrm{suc}\bigcup \left({A}\cup {B}\right)$
168 167 unssad ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to {A}\subseteq \mathrm{suc}\bigcup \left({A}\cup {B}\right)$
169 df-ss ${⊢}{A}\subseteq \mathrm{suc}\bigcup \left({A}\cup {B}\right)↔{A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)={A}$
170 168 169 sylib ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to {A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)={A}$
171 170 fveq2d ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to {F}\left({A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)={F}\left({A}\right)$
172 167 unssbd ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to {B}\subseteq \mathrm{suc}\bigcup \left({A}\cup {B}\right)$
173 df-ss ${⊢}{B}\subseteq \mathrm{suc}\bigcup \left({A}\cup {B}\right)↔{B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)={B}$
174 172 173 sylib ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to {B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)={B}$
175 174 fveq2d ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to {F}\left({B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)={F}\left({B}\right)$
176 171 175 eqeq12d ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)={F}\left({B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)\right)↔{F}\left({A}\right)={F}\left({B}\right)\right)$
177 170 174 eqeq12d ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({A}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)={B}\cap \mathrm{suc}\bigcup \left({A}\cup {B}\right)↔{A}={B}\right)$
178 163 176 177 3imtr3d ${⊢}\left({A}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge {B}\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left({F}\left({A}\right)={F}\left({B}\right)\to {A}={B}\right)$