ackbij1lem12

		Ref	Expression
	Hypothesis	ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
	Assertion	ackbij1lem12	$⊢ (B \in (𝒫 ω \cap Fin) \land A \subseteq B) \to F (A) \subseteq F (B)$

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
2	1	ackbij1lem10	$⊢ F : 𝒫 ω \cap Fin ⟶ ω$
3	1	ackbij1lem11	$⊢ (B \in (𝒫 ω \cap Fin) \land A \subseteq B) \to A \in (𝒫 ω \cap Fin)$
4		ffvelcdm	$⊢ (F : 𝒫 ω \cap Fin ⟶ ω \land A \in (𝒫 ω \cap Fin)) \to F (A) \in ω$
5	2 3 4	sylancr	$⊢ (B \in (𝒫 ω \cap Fin) \land A \subseteq B) \to F (A) \in ω$
6		difssd	$⊢ (B \in (𝒫 ω \cap Fin) \land A \subseteq B) \to B ∖ A \subseteq B$
7	1	ackbij1lem11	$⊢ (B \in (𝒫 ω \cap Fin) \land B ∖ A \subseteq B) \to B ∖ A \in (𝒫 ω \cap Fin)$
8	6 7	syldan	$⊢ (B \in (𝒫 ω \cap Fin) \land A \subseteq B) \to B ∖ A \in (𝒫 ω \cap Fin)$
9		ffvelcdm	$⊢ (F : 𝒫 ω \cap Fin ⟶ ω \land B ∖ A \in (𝒫 ω \cap Fin)) \to F (B ∖ A) \in ω$
10	2 8 9	sylancr	$⊢ (B \in (𝒫 ω \cap Fin) \land A \subseteq B) \to F (B ∖ A) \in ω$
11		nnaword1	$⊢ (F (A) \in ω \land F (B ∖ A) \in ω) \to F (A) \subseteq F (A) +_{𝑜} F (B ∖ A)$
12	5 10 11	syl2anc	$⊢ (B \in (𝒫 ω \cap Fin) \land A \subseteq B) \to F (A) \subseteq F (A) +_{𝑜} F (B ∖ A)$
13		disjdif	$⊢ A \cap (B ∖ A) = \emptyset$
14	13	a1i	$⊢ (B \in (𝒫 ω \cap Fin) \land A \subseteq B) \to A \cap (B ∖ A) = \emptyset$
15	1	ackbij1lem9	$⊢ (A \in (𝒫 ω \cap Fin) \land B ∖ A \in (𝒫 ω \cap Fin) \land A \cap (B ∖ A) = \emptyset) \to F (A \cup (B ∖ A)) = F (A) +_{𝑜} F (B ∖ A)$
16	3 8 14 15	syl3anc	$⊢ (B \in (𝒫 ω \cap Fin) \land A \subseteq B) \to F (A \cup (B ∖ A)) = F (A) +_{𝑜} F (B ∖ A)$
17		undif	$⊢ A \subseteq B \leftrightarrow A \cup (B ∖ A) = B$
18	17	bilani	$⊢ (B \in (𝒫 ω \cap Fin) \land A \subseteq B) \to A \cup (B ∖ A) = B$
19	18	fveq2d	$⊢ (B \in (𝒫 ω \cap Fin) \land A \subseteq B) \to F (A \cup (B ∖ A)) = F (B)$
20	16 19	eqtr3d	$⊢ (B \in (𝒫 ω \cap Fin) \land A \subseteq B) \to F (A) +_{𝑜} F (B ∖ A) = F (B)$
21	12 20	sseqtrd	$⊢ (B \in (𝒫 ω \cap Fin) \land A \subseteq B) \to F (A) \subseteq F (B)$

Metamath Proof Explorer

Theorem ackbij1lem12

Proof