This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ackbij1lem16

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

Ref Expression
Hypothesis ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
Assertion ackbij1lem16 ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) → 𝐴 = 𝐵 ) )

Proof

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