Theorem incssnn0

Description: Transitivity induction of subsets, lemma for nacsfix . (Contributed by Stefan O'Rear, 4-Apr-2015)

	Ref	Expression
Assertion	incssnn0	$$⊢\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{Z}}_{\ge A}\right)\to F\left(A\right)\subseteq F\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢a=A\to F\left(a\right)=F\left(A\right)$$
2	1	sseq2d	$$⊢a=A\to \left(F\left(A\right)\subseteq F\left(a\right)\leftrightarrow F\left(A\right)\subseteq F\left(A\right)\right)$$
3	2	imbi2d	$$⊢a=A\to \left(\left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to F\left(A\right)\subseteq F\left(a\right)\right)\leftrightarrow \left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to F\left(A\right)\subseteq F\left(A\right)\right)\right)$$
4		fveq2	$$⊢a=b\to F\left(a\right)=F\left(b\right)$$
5	4	sseq2d	$$⊢a=b\to \left(F\left(A\right)\subseteq F\left(a\right)\leftrightarrow F\left(A\right)\subseteq F\left(b\right)\right)$$
6	5	imbi2d	$$⊢a=b\to \left(\left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to F\left(A\right)\subseteq F\left(a\right)\right)\leftrightarrow \left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to F\left(A\right)\subseteq F\left(b\right)\right)\right)$$
7		fveq2	$$⊢a=b+1\to F\left(a\right)=F\left(b+1\right)$$
8	7	sseq2d	$$⊢a=b+1\to \left(F\left(A\right)\subseteq F\left(a\right)\leftrightarrow F\left(A\right)\subseteq F\left(b+1\right)\right)$$
9	8	imbi2d	$$⊢a=b+1\to \left(\left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to F\left(A\right)\subseteq F\left(a\right)\right)\leftrightarrow \left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to F\left(A\right)\subseteq F\left(b+1\right)\right)\right)$$
10		fveq2	$$⊢a=B\to F\left(a\right)=F\left(B\right)$$
11	10	sseq2d	$$⊢a=B\to \left(F\left(A\right)\subseteq F\left(a\right)\leftrightarrow F\left(A\right)\subseteq F\left(B\right)\right)$$
12	11	imbi2d	$$⊢a=B\to \left(\left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to F\left(A\right)\subseteq F\left(a\right)\right)\leftrightarrow \left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to F\left(A\right)\subseteq F\left(B\right)\right)\right)$$
13		ssid	$$⊢F\left(A\right)\subseteq F\left(A\right)$$
14	13	2a1i	$$⊢A\in \mathbb{Z}\to \left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to F\left(A\right)\subseteq F\left(A\right)\right)$$
15		eluznn0	$$⊢\left(A\in {\mathbb{N}}_0\wedge b\in {\mathbb{Z}}_{\ge A}\right)\to b\in {\mathbb{N}}_0$$
16	15	ancoms	$$⊢\left(b\in {\mathbb{Z}}_{\ge A}\wedge A\in {\mathbb{N}}_0\right)\to b\in {\mathbb{N}}_0$$
17		fveq2	$$⊢x=b\to F\left(x\right)=F\left(b\right)$$
18		fvoveq1	$$⊢x=b\to F\left(x+1\right)=F\left(b+1\right)$$
19	17 18	sseq12d	$$⊢x=b\to \left(F\left(x\right)\subseteq F\left(x+1\right)\leftrightarrow F\left(b\right)\subseteq F\left(b+1\right)\right)$$
20	19	rspcv	$$⊢b\in {\mathbb{N}}_0\to \left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\to F\left(b\right)\subseteq F\left(b+1\right)\right)$$
21	16 20	syl	$$⊢\left(b\in {\mathbb{Z}}_{\ge A}\wedge A\in {\mathbb{N}}_0\right)\to \left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\to F\left(b\right)\subseteq F\left(b+1\right)\right)$$
22	21	expimpd	$$⊢b\in {\mathbb{Z}}_{\ge A}\to \left(\left(A\in {\mathbb{N}}_0\wedge \forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\right)\to F\left(b\right)\subseteq F\left(b+1\right)\right)$$
23	22	ancomsd	$$⊢b\in {\mathbb{Z}}_{\ge A}\to \left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to F\left(b\right)\subseteq F\left(b+1\right)\right)$$
24		sstr2	$$⊢F\left(A\right)\subseteq F\left(b\right)\to \left(F\left(b\right)\subseteq F\left(b+1\right)\to F\left(A\right)\subseteq F\left(b+1\right)\right)$$
25	24	com12	$$⊢F\left(b\right)\subseteq F\left(b+1\right)\to \left(F\left(A\right)\subseteq F\left(b\right)\to F\left(A\right)\subseteq F\left(b+1\right)\right)$$
26	23 25	syl6	$$⊢b\in {\mathbb{Z}}_{\ge A}\to \left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to \left(F\left(A\right)\subseteq F\left(b\right)\to F\left(A\right)\subseteq F\left(b+1\right)\right)\right)$$
27	26	a2d	$$⊢b\in {\mathbb{Z}}_{\ge A}\to \left(\left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to F\left(A\right)\subseteq F\left(b\right)\right)\to \left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to F\left(A\right)\subseteq F\left(b+1\right)\right)\right)$$
28	3 6 9 12 14 27	uzind4	$$⊢B\in {\mathbb{Z}}_{\ge A}\to \left(\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to F\left(A\right)\subseteq F\left(B\right)\right)$$
29	28	com12	$$⊢\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\right)\to \left(B\in {\mathbb{Z}}_{\ge A}\to F\left(A\right)\subseteq F\left(B\right)\right)$$
30	29	3impia	$$⊢\left(\forall x\in {\mathbb{N}}_{0}F\left(x\right)\subseteq F\left(x+1\right)\wedge A\in {\mathbb{N}}_0\wedge B\in {\mathbb{Z}}_{\ge A}\right)\to F\left(A\right)\subseteq F\left(B\right)$$