Metamath Proof Explorer

Theorem ackbij1lem12

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

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

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2 1 ackbij1lem10 ⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω
3 1 ackbij1lem11 ⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ∈ ( 𝒫 ω ∩ Fin ) )
4 ffvelcdm ⊢ ( ( 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω ∧ 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ω )
5 2 3 4 sylancr ⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ ω )
6 difssd ⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐵 ∖ 𝐴 ) ⊆ 𝐵 )
7 1 ackbij1lem11 ⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐵 ∖ 𝐴 ) ⊆ 𝐵 ) → ( 𝐵 ∖ 𝐴 ) ∈ ( 𝒫 ω ∩ Fin ) )
8 6 7 syldan ⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐵 ∖ 𝐴 ) ∈ ( 𝒫 ω ∩ Fin ) )
9 ffvelcdm ⊢ ( ( 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω ∧ ( 𝐵 ∖ 𝐴 ) ∈ ( 𝒫 ω ∩ Fin ) ) → ( 𝐹 ‘ ( 𝐵 ∖ 𝐴 ) ) ∈ ω )
10 2 8 9 sylancr ⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝐵 ∖ 𝐴 ) ) ∈ ω )
11 nnaword1 ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ω ∧ ( 𝐹 ‘ ( 𝐵 ∖ 𝐴 ) ) ∈ ω ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( ( 𝐹 ‘ 𝐴 ) +o ( 𝐹 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
12 5 10 11 syl2anc ⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( ( 𝐹 ‘ 𝐴 ) +o ( 𝐹 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
13 disjdif ⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
14 13 a1i ⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅ )
15 1 ackbij1lem9 ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐵 ∖ 𝐴 ) ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅ ) → ( 𝐹 ‘ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( ( 𝐹 ‘ 𝐴 ) +o ( 𝐹 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
16 3 8 14 15 syl3anc ⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( ( 𝐹 ‘ 𝐴 ) +o ( 𝐹 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
17 undif ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
18 17 biimpi ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
19 18 adantl ⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
20 19 fveq2d ⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( 𝐹 ‘ 𝐵 ) )
21 16 20 eqtr3d ⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝐹 ‘ 𝐴 ) +o ( 𝐹 ‘ ( 𝐵 ∖ 𝐴 ) ) ) = ( 𝐹 ‘ 𝐵 ) )
22 12 21 sseqtrd ⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) )