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	bilani	⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
19	18	fveq2d	⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( 𝐹 ‘ 𝐵 ) )
20	16 19	eqtr3d	⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝐹 ‘ 𝐴 ) +o ( 𝐹 ‘ ( 𝐵 ∖ 𝐴 ) ) ) = ( 𝐹 ‘ 𝐵 ) )
21	12 20	sseqtrd	⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) )