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 0fin ⊢ ∅ ∈ 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 ffvelrni ⊢ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) ∈ ω )
36 4 35 syl ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) ∈ ω )
37 ackbij1lem3 ⊢ ( ∩ ( ω ∖ 𝐴 ) ∈ ω → ∩ ( ω ∖ 𝐴 ) ∈ ( 𝒫 ω ∩ Fin ) )
38 19 37 syl ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ∩ ( ω ∖ 𝐴 ) ∈ ( 𝒫 ω ∩ Fin ) )
39 34 ffvelrni ⊢ ( ∩ ( ω ∖ 𝐴 ) ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ∈ ω )
40 38 39 syl ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ∈ ω )
41 nnasuc ⊢ ( ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) ∈ ω ∧ ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ∈ ω ) → ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o suc ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = suc ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) )
42 36 40 41 syl2anc ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o suc ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = suc ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) )
43 incom ⊢ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∩ ∩ ( ω ∖ 𝐴 ) ) = ( ∩ ( ω ∖ 𝐴 ) ∩ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) )
44 disjdif ⊢ ( ∩ ( ω ∖ 𝐴 ) ∩ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) = ∅
45 43 44 eqtri ⊢ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∩ ∩ ( ω ∖ 𝐴 ) ) = ∅
46 45 a1i ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∩ ∩ ( ω ∖ 𝐴 ) ) = ∅ )
47 1 ackbij1lem9 ⊢ ( ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∈ ( 𝒫 ω ∩ Fin ) ∧ ∩ ( ω ∖ 𝐴 ) ∈ ( 𝒫 ω ∩ Fin ) ∧ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∩ ∩ ( ω ∖ 𝐴 ) ) = ∅ ) → ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ ∩ ( ω ∖ 𝐴 ) ) ) = ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) )
48 4 38 46 47 syl3anc ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ ∩ ( ω ∖ 𝐴 ) ) ) = ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) )
49 uncom ⊢ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ ∩ ( ω ∖ 𝐴 ) ) = ( ∩ ( ω ∖ 𝐴 ) ∪ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) )
50 onnmin ⊢ ( ( ( ω ∖ 𝐴 ) ⊆ On ∧ 𝑎 ∈ ( ω ∖ 𝐴 ) ) → ¬ 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) )
51 7 50 mpan ⊢ ( 𝑎 ∈ ( ω ∖ 𝐴 ) → ¬ 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) )
52 51 con2i ⊢ ( 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) → ¬ 𝑎 ∈ ( ω ∖ 𝐴 ) )
53 52 adantl ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) ) → ¬ 𝑎 ∈ ( ω ∖ 𝐴 ) )
54 ordom ⊢ Ord ω
55 ordelss ⊢ ( ( Ord ω ∧ ∩ ( ω ∖ 𝐴 ) ∈ ω ) → ∩ ( ω ∖ 𝐴 ) ⊆ ω )
56 54 19 55 sylancr ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ∩ ( ω ∖ 𝐴 ) ⊆ ω )
57 56 sselda ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) ) → 𝑎 ∈ ω )
58 eldif ⊢ ( 𝑎 ∈ ( ω ∖ 𝐴 ) ↔ ( 𝑎 ∈ ω ∧ ¬ 𝑎 ∈ 𝐴 ) )
59 58 simplbi2 ⊢ ( 𝑎 ∈ ω → ( ¬ 𝑎 ∈ 𝐴 → 𝑎 ∈ ( ω ∖ 𝐴 ) ) )
60 59 orrd ⊢ ( 𝑎 ∈ ω → ( 𝑎 ∈ 𝐴 ∨ 𝑎 ∈ ( ω ∖ 𝐴 ) ) )
61 60 orcomd ⊢ ( 𝑎 ∈ ω → ( 𝑎 ∈ ( ω ∖ 𝐴 ) ∨ 𝑎 ∈ 𝐴 ) )
62 57 61 syl ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) ) → ( 𝑎 ∈ ( ω ∖ 𝐴 ) ∨ 𝑎 ∈ 𝐴 ) )
63 orel1 ⊢ ( ¬ 𝑎 ∈ ( ω ∖ 𝐴 ) → ( ( 𝑎 ∈ ( ω ∖ 𝐴 ) ∨ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 ) )
64 53 62 63 sylc ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) ) → 𝑎 ∈ 𝐴 )
65 64 ex ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝑎 ∈ ∩ ( ω ∖ 𝐴 ) → 𝑎 ∈ 𝐴 ) )
66 65 ssrdv ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ∩ ( ω ∖ 𝐴 ) ⊆ 𝐴 )
67 undif ⊢ ( ∩ ( ω ∖ 𝐴 ) ⊆ 𝐴 ↔ ( ∩ ( ω ∖ 𝐴 ) ∪ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) = 𝐴 )
68 66 67 sylib ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ∩ ( ω ∖ 𝐴 ) ∪ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) = 𝐴 )
69 49 68 syl5eq ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ ∩ ( ω ∖ 𝐴 ) ) = 𝐴 )
70 69 fveq2d ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ ∩ ( ω ∖ 𝐴 ) ) ) = ( 𝐹 ‘ 𝐴 ) )
71 48 70 eqtr3d ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = ( 𝐹 ‘ 𝐴 ) )
72 suceq ⊢ ( ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = ( 𝐹 ‘ 𝐴 ) → suc ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = suc ( 𝐹 ‘ 𝐴 ) )
73 71 72 syl ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → suc ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = suc ( 𝐹 ‘ 𝐴 ) )
74 42 73 eqtrd ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( ( 𝐹 ‘ ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ) +o suc ( 𝐹 ‘ ∩ ( ω ∖ 𝐴 ) ) ) = suc ( 𝐹 ‘ 𝐴 ) )
75 30 33 74 3eqtrd ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) ) = suc ( 𝐹 ‘ 𝐴 ) )
76 fveqeq2 ⊢ ( 𝑏 = ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) → ( ( 𝐹 ‘ 𝑏 ) = suc ( 𝐹 ‘ 𝐴 ) ↔ ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) ) = suc ( 𝐹 ‘ 𝐴 ) ) )
77 76 rspcev ⊢ ( ( ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐹 ‘ ( ( 𝐴 ∖ ∩ ( ω ∖ 𝐴 ) ) ∪ { ∩ ( ω ∖ 𝐴 ) } ) ) = suc ( 𝐹 ‘ 𝐴 ) ) → ∃ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑏 ) = suc ( 𝐹 ‘ 𝐴 ) )
78 23 75 77 syl2anc ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ∃ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( 𝐹 ‘ 𝑏 ) = suc ( 𝐹 ‘ 𝐴 ) )