Theorem fin23lem36

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

	Ref	Expression
Hypotheses	fin23lem33.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
	fin23lem.f	⊢ ( 𝜑 → ℎ : ω –1-1→ V )
	fin23lem.g	⊢ ( 𝜑 → ∪ ran ℎ ⊆ 𝐺 )
	fin23lem.h	⊢ ( 𝜑 → ∀ 𝑗 ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) )
	fin23lem.i	⊢ 𝑌 = ( rec ( 𝑖 , ℎ ) ↾ ω )
Assertion	fin23lem36	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝜑 ) ) → ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fin23lem33.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
2		fin23lem.f	⊢ ( 𝜑 → ℎ : ω –1-1→ V )
3		fin23lem.g	⊢ ( 𝜑 → ∪ ran ℎ ⊆ 𝐺 )
4		fin23lem.h	⊢ ( 𝜑 → ∀ 𝑗 ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) )
5		fin23lem.i	⊢ 𝑌 = ( rec ( 𝑖 , ℎ ) ↾ ω )
6		fveq2	⊢ ( 𝑎 = 𝐵 → ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ 𝐵 ) )
7	6	rneqd	⊢ ( 𝑎 = 𝐵 → ran ( 𝑌 ‘ 𝑎 ) = ran ( 𝑌 ‘ 𝐵 ) )
8	7	unieqd	⊢ ( 𝑎 = 𝐵 → ∪ ran ( 𝑌 ‘ 𝑎 ) = ∪ ran ( 𝑌 ‘ 𝐵 ) )
9	8	sseq1d	⊢ ( 𝑎 = 𝐵 → ( ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ↔ ∪ ran ( 𝑌 ‘ 𝐵 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
10	9	imbi2d	⊢ ( 𝑎 = 𝐵 → ( ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ↔ ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝐵 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ) )
11		fveq2	⊢ ( 𝑎 = 𝑏 → ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ 𝑏 ) )
12	11	rneqd	⊢ ( 𝑎 = 𝑏 → ran ( 𝑌 ‘ 𝑎 ) = ran ( 𝑌 ‘ 𝑏 ) )
13	12	unieqd	⊢ ( 𝑎 = 𝑏 → ∪ ran ( 𝑌 ‘ 𝑎 ) = ∪ ran ( 𝑌 ‘ 𝑏 ) )
14	13	sseq1d	⊢ ( 𝑎 = 𝑏 → ( ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ↔ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
15	14	imbi2d	⊢ ( 𝑎 = 𝑏 → ( ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ↔ ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ) )
16		fveq2	⊢ ( 𝑎 = suc 𝑏 → ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ suc 𝑏 ) )
17	16	rneqd	⊢ ( 𝑎 = suc 𝑏 → ran ( 𝑌 ‘ 𝑎 ) = ran ( 𝑌 ‘ suc 𝑏 ) )
18	17	unieqd	⊢ ( 𝑎 = suc 𝑏 → ∪ ran ( 𝑌 ‘ 𝑎 ) = ∪ ran ( 𝑌 ‘ suc 𝑏 ) )
19	18	sseq1d	⊢ ( 𝑎 = suc 𝑏 → ( ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ↔ ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
20	19	imbi2d	⊢ ( 𝑎 = suc 𝑏 → ( ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ↔ ( 𝜑 → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ) )
21		fveq2	⊢ ( 𝑎 = 𝐴 → ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ 𝐴 ) )
22	21	rneqd	⊢ ( 𝑎 = 𝐴 → ran ( 𝑌 ‘ 𝑎 ) = ran ( 𝑌 ‘ 𝐴 ) )
23	22	unieqd	⊢ ( 𝑎 = 𝐴 → ∪ ran ( 𝑌 ‘ 𝑎 ) = ∪ ran ( 𝑌 ‘ 𝐴 ) )
24	23	sseq1d	⊢ ( 𝑎 = 𝐴 → ( ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ↔ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
25	24	imbi2d	⊢ ( 𝑎 = 𝐴 → ( ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ↔ ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ) )
26		ssid	⊢ ∪ ran ( 𝑌 ‘ 𝐵 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 )
27	26	2a1i	⊢ ( 𝐵 ∈ ω → ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝐵 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
28		simprr	⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝑏 ∧ 𝜑 ) ) → 𝜑 )
29		simpll	⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝑏 ∧ 𝜑 ) ) → 𝑏 ∈ ω )
30	1 2 3 4 5	fin23lem35	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ω ) → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) )
31	28 29 30	syl2anc	⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝑏 ∧ 𝜑 ) ) → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) )
32	31	pssssd	⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝑏 ∧ 𝜑 ) ) → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝑏 ) )
33		sstr2	⊢ ( ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝑏 ) → ( ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
34	32 33	syl	⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝑏 ∧ 𝜑 ) ) → ( ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
35	34	expr	⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑏 ) → ( 𝜑 → ( ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ) )
36	35	a2d	⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑏 ) → ( ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) → ( 𝜑 → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ) )
37	10 15 20 25 27 36	findsg	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
38	37	impr	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝜑 ) ) → ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) )