fin23lem36

Description: Lemma for fin23 . Weak order property of Y . (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Hypotheses	fin23lem33.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
	fin23lem.f	$⊢ φ \to h : ω \underset{1-1}{⟶} V$
	fin23lem.g	$⊢ φ \to ⋃ ran h \subseteq G$
	fin23lem.h	$⊢ φ \to \forall j ((j : ω \underset{1-1}{⟶} V \land ⋃ ran j \subseteq G) \to (i (j) : ω \underset{1-1}{⟶} V \land ⋃ ran i (j) \subset ⋃ ran j))$
	fin23lem.i	$⊢ Y = {rec (i, h) ↾}_{ω}$
Assertion	fin23lem36	$⊢ ((A \in ω \land B \in ω) \land (B \subseteq A \land φ)) \to ⋃ ran Y (A) \subseteq ⋃ ran Y (B)$

Proof

Step	Hyp	Ref	Expression
1		fin23lem33.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
2		fin23lem.f	$⊢ φ \to h : ω \underset{1-1}{⟶} V$
3		fin23lem.g	$⊢ φ \to ⋃ ran h \subseteq G$
4		fin23lem.h	$⊢ φ \to \forall j ((j : ω \underset{1-1}{⟶} V \land ⋃ ran j \subseteq G) \to (i (j) : ω \underset{1-1}{⟶} V \land ⋃ ran i (j) \subset ⋃ ran j))$
5		fin23lem.i	$⊢ Y = {rec (i, h) ↾}_{ω}$
6		fveq2	$⊢ a = B \to Y (a) = Y (B)$
7	6	rneqd	$⊢ a = B \to ran Y (a) = ran Y (B)$
8	7	unieqd	$⊢ a = B \to ⋃ ran Y (a) = ⋃ ran Y (B)$
9	8	sseq1d	$⊢ a = B \to (⋃ ran Y (a) \subseteq ⋃ ran Y (B) \leftrightarrow ⋃ ran Y (B) \subseteq ⋃ ran Y (B))$
10	9	imbi2d	$⊢ a = B \to ((φ \to ⋃ ran Y (a) \subseteq ⋃ ran Y (B)) \leftrightarrow (φ \to ⋃ ran Y (B) \subseteq ⋃ ran Y (B)))$
11		fveq2	$⊢ a = b \to Y (a) = Y (b)$
12	11	rneqd	$⊢ a = b \to ran Y (a) = ran Y (b)$
13	12	unieqd	$⊢ a = b \to ⋃ ran Y (a) = ⋃ ran Y (b)$
14	13	sseq1d	$⊢ a = b \to (⋃ ran Y (a) \subseteq ⋃ ran Y (B) \leftrightarrow ⋃ ran Y (b) \subseteq ⋃ ran Y (B))$
15	14	imbi2d	$⊢ a = b \to ((φ \to ⋃ ran Y (a) \subseteq ⋃ ran Y (B)) \leftrightarrow (φ \to ⋃ ran Y (b) \subseteq ⋃ ran Y (B)))$
16		fveq2	$⊢ a = suc b \to Y (a) = Y (suc b)$
17	16	rneqd	$⊢ a = suc b \to ran Y (a) = ran Y (suc b)$
18	17	unieqd	$⊢ a = suc b \to ⋃ ran Y (a) = ⋃ ran Y (suc b)$
19	18	sseq1d	$⊢ a = suc b \to (⋃ ran Y (a) \subseteq ⋃ ran Y (B) \leftrightarrow ⋃ ran Y (suc b) \subseteq ⋃ ran Y (B))$
20	19	imbi2d	$⊢ a = suc b \to ((φ \to ⋃ ran Y (a) \subseteq ⋃ ran Y (B)) \leftrightarrow (φ \to ⋃ ran Y (suc b) \subseteq ⋃ ran Y (B)))$
21		fveq2	$⊢ a = A \to Y (a) = Y (A)$
22	21	rneqd	$⊢ a = A \to ran Y (a) = ran Y (A)$
23	22	unieqd	$⊢ a = A \to ⋃ ran Y (a) = ⋃ ran Y (A)$
24	23	sseq1d	$⊢ a = A \to (⋃ ran Y (a) \subseteq ⋃ ran Y (B) \leftrightarrow ⋃ ran Y (A) \subseteq ⋃ ran Y (B))$
25	24	imbi2d	$⊢ a = A \to ((φ \to ⋃ ran Y (a) \subseteq ⋃ ran Y (B)) \leftrightarrow (φ \to ⋃ ran Y (A) \subseteq ⋃ ran Y (B)))$
26		ssid	$⊢ ⋃ ran Y (B) \subseteq ⋃ ran Y (B)$
27	26	2a1i	$⊢ B \in ω \to (φ \to ⋃ ran Y (B) \subseteq ⋃ ran Y (B))$
28		simprr	$⊢ ((b \in ω \land B \in ω) \land (B \subseteq b \land φ)) \to φ$
29		simpll	$⊢ ((b \in ω \land B \in ω) \land (B \subseteq b \land φ)) \to b \in ω$
30	1 2 3 4 5	fin23lem35	$⊢ (φ \land b \in ω) \to ⋃ ran Y (suc b) \subset ⋃ ran Y (b)$
31	28 29 30	syl2anc	$⊢ ((b \in ω \land B \in ω) \land (B \subseteq b \land φ)) \to ⋃ ran Y (suc b) \subset ⋃ ran Y (b)$
32	31	pssssd	$⊢ ((b \in ω \land B \in ω) \land (B \subseteq b \land φ)) \to ⋃ ran Y (suc b) \subseteq ⋃ ran Y (b)$
33		sstr2	$⊢ ⋃ ran Y (suc b) \subseteq ⋃ ran Y (b) \to (⋃ ran Y (b) \subseteq ⋃ ran Y (B) \to ⋃ ran Y (suc b) \subseteq ⋃ ran Y (B))$
34	32 33	syl	$⊢ ((b \in ω \land B \in ω) \land (B \subseteq b \land φ)) \to (⋃ ran Y (b) \subseteq ⋃ ran Y (B) \to ⋃ ran Y (suc b) \subseteq ⋃ ran Y (B))$
35	34	expr	$⊢ ((b \in ω \land B \in ω) \land B \subseteq b) \to (φ \to (⋃ ran Y (b) \subseteq ⋃ ran Y (B) \to ⋃ ran Y (suc b) \subseteq ⋃ ran Y (B)))$
36	35	a2d	$⊢ ((b \in ω \land B \in ω) \land B \subseteq b) \to ((φ \to ⋃ ran Y (b) \subseteq ⋃ ran Y (B)) \to (φ \to ⋃ ran Y (suc b) \subseteq ⋃ ran Y (B)))$
37	10 15 20 25 27 36	findsg	$⊢ ((A \in ω \land B \in ω) \land B \subseteq A) \to (φ \to ⋃ ran Y (A) \subseteq ⋃ ran Y (B))$
38	37	impr	$⊢ ((A \in ω \land B \in ω) \land (B \subseteq A \land φ)) \to ⋃ ran Y (A) \subseteq ⋃ ran Y (B)$

Metamath Proof Explorer

Theorem fin23lem36

Proof