volsuplem

		Ref	Expression
	Assertion	volsuplem	$⊢ (\forall n \in ℕ F (n) \subseteq F (n + 1) \land (A \in ℕ \land B \in ℤ_{\geq A})) \to F (A) \subseteq F (B)$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = A \to F (x) = F (A)$
2	1	sseq2d	$⊢ x = A \to (F (A) \subseteq F (x) \leftrightarrow F (A) \subseteq F (A))$
3	2	imbi2d	$⊢ x = A \to (((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to F (A) \subseteq F (x)) \leftrightarrow ((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to F (A) \subseteq F (A)))$
4		fveq2	$⊢ x = k \to F (x) = F (k)$
5	4	sseq2d	$⊢ x = k \to (F (A) \subseteq F (x) \leftrightarrow F (A) \subseteq F (k))$
6	5	imbi2d	$⊢ x = k \to (((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to F (A) \subseteq F (x)) \leftrightarrow ((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to F (A) \subseteq F (k)))$
7		fveq2	$⊢ x = k + 1 \to F (x) = F (k + 1)$
8	7	sseq2d	$⊢ x = k + 1 \to (F (A) \subseteq F (x) \leftrightarrow F (A) \subseteq F (k + 1))$
9	8	imbi2d	$⊢ x = k + 1 \to (((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to F (A) \subseteq F (x)) \leftrightarrow ((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to F (A) \subseteq F (k + 1)))$
10		fveq2	$⊢ x = B \to F (x) = F (B)$
11	10	sseq2d	$⊢ x = B \to (F (A) \subseteq F (x) \leftrightarrow F (A) \subseteq F (B))$
12	11	imbi2d	$⊢ x = B \to (((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to F (A) \subseteq F (x)) \leftrightarrow ((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to F (A) \subseteq F (B)))$
13		ssid	$⊢ F (A) \subseteq F (A)$
14	13	2a1i	$⊢ A \in ℤ \to ((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to F (A) \subseteq F (A))$
15		eluznn	$⊢ (A \in ℕ \land k \in ℤ_{\geq A}) \to k \in ℕ$
16		fveq2	$⊢ n = k \to F (n) = F (k)$
17		fvoveq1	$⊢ n = k \to F (n + 1) = F (k + 1)$
18	16 17	sseq12d	$⊢ n = k \to (F (n) \subseteq F (n + 1) \leftrightarrow F (k) \subseteq F (k + 1))$
19	18	rspccva	$⊢ (\forall n \in ℕ F (n) \subseteq F (n + 1) \land k \in ℕ) \to F (k) \subseteq F (k + 1)$
20	15 19	sylan2	$⊢ (\forall n \in ℕ F (n) \subseteq F (n + 1) \land (A \in ℕ \land k \in ℤ_{\geq A})) \to F (k) \subseteq F (k + 1)$
21	20	anassrs	$⊢ ((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \land k \in ℤ_{\geq A}) \to F (k) \subseteq F (k + 1)$
22		sstr2	$⊢ F (A) \subseteq F (k) \to (F (k) \subseteq F (k + 1) \to F (A) \subseteq F (k + 1))$
23	21 22	syl5com	$⊢ ((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \land k \in ℤ_{\geq A}) \to (F (A) \subseteq F (k) \to F (A) \subseteq F (k + 1))$
24	23	expcom	$⊢ k \in ℤ_{\geq A} \to ((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to (F (A) \subseteq F (k) \to F (A) \subseteq F (k + 1)))$
25	24	a2d	$⊢ k \in ℤ_{\geq A} \to (((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to F (A) \subseteq F (k)) \to ((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to F (A) \subseteq F (k + 1)))$
26	3 6 9 12 14 25	uzind4	$⊢ B \in ℤ_{\geq A} \to ((\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to F (A) \subseteq F (B))$
27	26	com12	$⊢ (\forall n \in ℕ F (n) \subseteq F (n + 1) \land A \in ℕ) \to (B \in ℤ_{\geq A} \to F (A) \subseteq F (B))$
28	27	impr	$⊢ (\forall n \in ℕ F (n) \subseteq F (n + 1) \land (A \in ℕ \land B \in ℤ_{\geq A})) \to F (A) \subseteq F (B)$

Metamath Proof Explorer

Theorem volsuplem

Proof