Metamath Proof Explorer

Theorem ackbij1lem18

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

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

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2 difss ⊢ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ⊆ 𝐴
3 1 ackbij1lem11 ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ⊆ 𝐴 ) → ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∈ ( 𝒫 ω ∩ Fin ) )
4 2 3 mpan2 ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∈ ( 𝒫 ω ∩ Fin ) )
5 difss ⊢ ( ω ∖ 𝐴 ) ⊆ ω
6 omsson ⊢ ω ⊆ On
7 5 6 sstri ⊢ ( ω ∖ 𝐴 ) ⊆ On
8 ominf ⊢ ¬ ω ∈ Fin
9 elinel2 ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ∈ Fin )
10 difinf ⊢ ( ( ¬ ω ∈ Fin ∧ 𝐴 ∈ Fin ) → ¬ ( ω ∖ 𝐴 ) ∈ Fin )
11 8 9 10 sylancr ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ¬ ( ω ∖ 𝐴 ) ∈ Fin )
12 0fi ⊢ ∅ ∈ Fin
13 eleq1 ⊢ ( ( ω ∖ 𝐴 ) = ∅ → ( ( ω ∖ 𝐴 ) ∈ Fin ↔ ∅ ∈ Fin ) )
14 12 13 mpbiri ⊢ ( ( ω ∖ 𝐴 ) = ∅ → ( ω ∖ 𝐴 ) ∈ Fin )
15 14 necon3bi ⊢ ( ¬ ( ω ∖ 𝐴 ) ∈ Fin → ( ω ∖ 𝐴 ) ≠ ∅ )
16 11 15 syl ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ω ∖ 𝐴 ) ≠ ∅ )
17 onint ⊢ ( ( ( ω ∖ 𝐴 ) ⊆ On ∧ ( ω ∖ 𝐴 ) ≠ ∅ ) → ∩ ( ω ∖ 𝐴 ) ∈ ( ω ∖ 𝐴 ) )
18 7 16 17 sylancr ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ∩ ( ω ∖ 𝐴 ) ∈ ( ω ∖ 𝐴 ) )
19 18 eldifad ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ∩ ( ω ∖ 𝐴 ) ∈ ω )
20 ackbij1lem4 ⊢ ( ∩ ( ω ∖ 𝐴 ) ∈ ω → { ∩ ( ω ∖ 𝐴 ) } ∈ ( 𝒫 ω ∩ Fin ) )
21 19 20 syl ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → { ∩ ( ω ∖ 𝐴 ) } ∈ ( 𝒫 ω ∩ Fin ) )
22 ackbij1lem6 ⊢ ( ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∈ ( 𝒫 ω ∩ Fin ) ∧ { ∩ ( ω ∖ 𝐴 ) } ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) ∈ ( 𝒫 ω ∩ Fin ) )
23 4 21 22 syl2anc ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) ∈ ( 𝒫 ω ∩ Fin ) )
24 18 eldifbd ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ¬ ∩ ( ω ∖ 𝐴 ) ∈ 𝐴 )
25 disjsn ⊢ ( ( 𝐴 ∩ { ∩ ( ω ∖ 𝐴 ) } ) = ∅ ↔ ¬ ∩ ( ω ∖ 𝐴 ) ∈ 𝐴 )
26 24 25 sylibr ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐴 ∩ { ∩ ( ω ∖ 𝐴 ) } ) = ∅ )
27 ssdisj ⊢ ( ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ⊆ 𝐴 ∧ ( 𝐴 ∩ { ∩ ( ω ∖ 𝐴 ) } ) = ∅ ) → ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∩ { ∩ ( ω ∖ 𝐴 ) } ) = ∅ )
28 2 26 27 sylancr ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∩ { ∩ ( ω ∖ 𝐴 ) } ) = ∅ )
29 1 ackbij1lem9 ⊢ ( ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∈ ( 𝒫 ω ∩ Fin ) ∧ { ∩ ( ω ∖ 𝐴 ) } ∈ ( 𝒫 ω ∩ Fin ) ∧ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∩ { ∩ ( ω ∖ 𝐴 ) } ) = ∅ ) → ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) ) = ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ { ∩ ( ω ∖ 𝐴 ) } ) ) )
30 4 21 28 29 syl3anc ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) ) = ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ { ∩ ( ω ∖ 𝐴 ) } ) ) )
31 1 ackbij1lem14 ⊢ ( ∩ ( ω ∖ 𝐴 ) ∈ ω → ( 𝐹 ‘ { ∩ ( ω ∖ 𝐴 ) } ) = suc ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) )
32 19 31 syl ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ { ∩ ( ω ∖ 𝐴 ) } ) = suc ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) )
33 32 oveq2d ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ { ∩ ( ω ∖ 𝐴 ) } ) ) = ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o suc ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) )
34 1 ackbij1lem10 ⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω
35 34 ffvelcdmi ⊢ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) ∈ ω )
36 4 35 syl ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) ∈ ω )
37 ackbij1lem3 ⊢ ( ∩ ( ω ∖ 𝐴 ) ∈ ω → ∩ ( ω ∖ 𝐴 ) ∈ ( 𝒫 ω ∩ Fin ) )
38 19 37 syl ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ∩ ( ω ∖ 𝐴 ) ∈ ( 𝒫 ω ∩ Fin ) )
39 34 ffvelcdmi ⊢ ( ∩ ( ω ∖ 𝐴 ) ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ∈ ω )
40 38 39 syl ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ∈ ω )
41 nnasuc ⊢ ( ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) ∈ ω ∧ ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ∈ ω ) → ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o suc ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = suc ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) )
42 36 40 41 syl2anc ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o suc ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = suc ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) )
43 disjdifr ⊢ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∩ ∩ ( ω ∖ 𝐴 ) ) = ∅
44 43 a1i ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∩ ∩ ( ω ∖ 𝐴 ) ) = ∅ )
45 1 ackbij1lem9 ⊢ ( ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∈ ( 𝒫 ω ∩ Fin ) ∧ ∩ ( ω ∖ 𝐴 ) ∈ ( 𝒫 ω ∩ Fin ) ∧ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∩ ∩ ( ω ∖ 𝐴 ) ) = ∅ ) → ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ ∩ ( ω ∖ 𝐴 ) ) ) = ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) )
46 4 38 44 45 syl3anc ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ ∩ ( ω ∖ 𝐴 ) ) ) = ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) )
47 uncom ⊢ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ ∩ ( ω ∖ 𝐴 ) ) = ( ∩ ( ω ∖ 𝐴 ) ∪ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) )
48 onnmin ⊢ ( ( ( ω ∖ 𝐴 ) ⊆ On ∧ 𝑎 ∈ ( ω ∖ 𝐴 ) ) → ¬ 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) )
49 7 48 mpan ⊢ ( 𝑎 ∈ ( ω ∖ 𝐴 ) → ¬ 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) )
50 49 con2i ⊢ ( 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) → ¬ 𝑎 ∈ ( ω ∖ 𝐴 ) )
51 50 adantl ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) ) → ¬ 𝑎 ∈ ( ω ∖ 𝐴 ) )
52 ordom ⊢ Ord ω
53 ordelss ⊢ ( ( Ord ω ∧ ∩ ( ω ∖ 𝐴 ) ∈ ω ) → ∩ ( ω ∖ 𝐴 ) ⊆ ω )
54 52 19 53 sylancr ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ∩ ( ω ∖ 𝐴 ) ⊆ ω )
55 54 sselda ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) ) → 𝑎 ∈ ω )
56 eldif ⊢ ( 𝑎 ∈ ( ω ∖ 𝐴 ) ↔ ( 𝑎 ∈ ω ∧ ¬ 𝑎 ∈ 𝐴 ) )
57 56 simplbi2 ⊢ ( 𝑎 ∈ ω → ( ¬ 𝑎 ∈ 𝐴 → 𝑎 ∈ ( ω ∖ 𝐴 ) ) )
58 57 orrd ⊢ ( 𝑎 ∈ ω → ( 𝑎 ∈ 𝐴 ∨ 𝑎 ∈ ( ω ∖ 𝐴 ) ) )
59 58 orcomd ⊢ ( 𝑎 ∈ ω → ( 𝑎 ∈ ( ω ∖ 𝐴 ) ∨ 𝑎 ∈ 𝐴 ) )
60 55 59 syl ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) ) → ( 𝑎 ∈ ( ω ∖ 𝐴 ) ∨ 𝑎 ∈ 𝐴 ) )
61 orel1 ⊢ ( ¬ 𝑎 ∈ ( ω ∖ 𝐴 ) → ( ( 𝑎 ∈ ( ω ∖ 𝐴 ) ∨ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 ) )
62 51 60 61 sylc ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) ) → 𝑎 ∈ 𝐴 )
63 62 ex ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) → 𝑎 ∈ 𝐴 ) )
64 63 ssrdv ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ∩ ( ω ∖ 𝐴 ) ⊆ 𝐴 )
65 undif ⊢ ( ∩ ( ω ∖ 𝐴 ) ⊆ 𝐴 ↔ ( ∩ ( ω ∖ 𝐴 ) ∪ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) = 𝐴 )
66 64 65 sylib ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ∩ ( ω ∖ 𝐴 ) ∪ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) = 𝐴 )
67 47 66 eqtrid ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ ∩ ( ω ∖ 𝐴 ) ) = 𝐴 )
68 67 fveq2d ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ ∩ ( ω ∖ 𝐴 ) ) ) = ( 𝐹 ‘ 𝐴 ) )
69 46 68 eqtr3d ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = ( 𝐹 ‘ 𝐴 ) )
70 suceq ⊢ ( ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = ( 𝐹 ‘ 𝐴 ) → suc ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = suc ( 𝐹 ‘ 𝐴 ) )
71 69 70 syl ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → suc ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = suc ( 𝐹 ‘ 𝐴 ) )
72 42 71 eqtrd ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o suc ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = suc ( 𝐹 ‘ 𝐴 ) )
73 30 33 72 3eqtrd ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) ) = suc ( 𝐹 ‘ 𝐴 ) )
74 fveqeq2 ⊢ ( 𝑏 = ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) → ( ( 𝐹 ‘ 𝑏 ) = suc ( 𝐹 ‘ 𝐴 ) ↔ ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) ) = suc ( 𝐹 ‘ 𝐴 ) ) )
75 74 rspcev ⊢ ( ( ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) ) = suc ( 𝐹 ‘ 𝐴 ) ) → ∃ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑏 ) = suc ( 𝐹 ‘ 𝐴 ) )
76 23 73 75 syl2anc ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ∃ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑏 ) = suc ( 𝐹 ‘ 𝐴 ) )