Theorem fin23lem31

Description: Lemma for fin23 . The residual is has a strictly smaller range than the previous sequence. This will be iterated to build an unbounded chain. (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Hypotheses	fin23lem.a	⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
	fin23lem17.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
	fin23lem.b	⊢ 𝑃 = { 𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) }
	fin23lem.c	⊢ 𝑄 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ 𝑃 ( 𝑥 ∩ 𝑃 ) ≈ 𝑤 ) )
	fin23lem.d	⊢ 𝑅 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ ( ω ∖ 𝑃 ) ( 𝑥 ∩ ( ω ∖ 𝑃 ) ) ≈ 𝑤 ) )
	fin23lem.e	⊢ 𝑍 = if ( 𝑃 ∈ Fin , ( 𝑡 ∘ 𝑅 ) , ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) )
Assertion	fin23lem31	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ 𝐺 ∈ 𝐹 ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ∪ ran 𝑍 ⊊ ∪ ran 𝑡 )

Proof

Step	Hyp	Ref	Expression
1		fin23lem.a	⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
2		fin23lem17.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
3		fin23lem.b	⊢ 𝑃 = { 𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) }
4		fin23lem.c	⊢ 𝑄 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ 𝑃 ( 𝑥 ∩ 𝑃 ) ≈ 𝑤 ) )
5		fin23lem.d	⊢ 𝑅 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ ( ω ∖ 𝑃 ) ( 𝑥 ∩ ( ω ∖ 𝑃 ) ) ≈ 𝑤 ) )
6		fin23lem.e	⊢ 𝑍 = if ( 𝑃 ∈ Fin , ( 𝑡 ∘ 𝑅 ) , ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) )
7	2	ssfin3ds	⊢ ( ( 𝐺 ∈ 𝐹 ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ∪ ran 𝑡 ∈ 𝐹 )
8	1 2 3 4 5 6	fin23lem29	⊢ ∪ ran 𝑍 ⊆ ∪ ran 𝑡
9	8	a1i	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ∪ ran 𝑡 ∈ 𝐹 ) → ∪ ran 𝑍 ⊆ ∪ ran 𝑡 )
10	1 2	fin23lem21	⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ∩ ran 𝑈 ≠ ∅ )
11	10	ancoms	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ∪ ran 𝑡 ∈ 𝐹 ) → ∩ ran 𝑈 ≠ ∅ )
12		n0	⊢ ( ∩ ran 𝑈 ≠ ∅ ↔ ∃ 𝑎 𝑎 ∈ ∩ ran 𝑈 )
13	11 12	sylib	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ∪ ran 𝑡 ∈ 𝐹 ) → ∃ 𝑎 𝑎 ∈ ∩ ran 𝑈 )
14	1	fnseqom	⊢ 𝑈 Fn ω
15		fndm	⊢ ( 𝑈 Fn ω → dom 𝑈 = ω )
16	14 15	ax-mp	⊢ dom 𝑈 = ω
17		peano1	⊢ ∅ ∈ ω
18	17	ne0ii	⊢ ω ≠ ∅
19	16 18	eqnetri	⊢ dom 𝑈 ≠ ∅
20		dm0rn0	⊢ ( dom 𝑈 = ∅ ↔ ran 𝑈 = ∅ )
21	20	necon3bii	⊢ ( dom 𝑈 ≠ ∅ ↔ ran 𝑈 ≠ ∅ )
22	19 21	mpbi	⊢ ran 𝑈 ≠ ∅
23		intssuni	⊢ ( ran 𝑈 ≠ ∅ → ∩ ran 𝑈 ⊆ ∪ ran 𝑈 )
24	22 23	ax-mp	⊢ ∩ ran 𝑈 ⊆ ∪ ran 𝑈
25	1	fin23lem16	⊢ ∪ ran 𝑈 = ∪ ran 𝑡
26	24 25	sseqtri	⊢ ∩ ran 𝑈 ⊆ ∪ ran 𝑡
27	26	sseli	⊢ ( 𝑎 ∈ ∩ ran 𝑈 → 𝑎 ∈ ∪ ran 𝑡 )
28		f1fun	⊢ ( 𝑡 : ω –1-1→ 𝑉 → Fun 𝑡 )
29	28	adantr	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ∪ ran 𝑡 ∈ 𝐹 ) → Fun 𝑡 )
30	1 2 3 4 5 6	fin23lem30	⊢ ( Fun 𝑡 → ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ∅ )
31	29 30	syl	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ∪ ran 𝑡 ∈ 𝐹 ) → ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ∅ )
32		disj	⊢ ( ( ∪ ran 𝑍 ∩ ∩ ran 𝑈 ) = ∅ ↔ ∀ 𝑎 ∈ ∪ ran 𝑍 ¬ 𝑎 ∈ ∩ ran 𝑈 )
33	31 32	sylib	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ∪ ran 𝑡 ∈ 𝐹 ) → ∀ 𝑎 ∈ ∪ ran 𝑍 ¬ 𝑎 ∈ ∩ ran 𝑈 )
34		rsp	⊢ ( ∀ 𝑎 ∈ ∪ ran 𝑍 ¬ 𝑎 ∈ ∩ ran 𝑈 → ( 𝑎 ∈ ∪ ran 𝑍 → ¬ 𝑎 ∈ ∩ ran 𝑈 ) )
35	33 34	syl	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ∪ ran 𝑡 ∈ 𝐹 ) → ( 𝑎 ∈ ∪ ran 𝑍 → ¬ 𝑎 ∈ ∩ ran 𝑈 ) )
36	35	con2d	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ∪ ran 𝑡 ∈ 𝐹 ) → ( 𝑎 ∈ ∩ ran 𝑈 → ¬ 𝑎 ∈ ∪ ran 𝑍 ) )
37	36	imp	⊢ ( ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ∪ ran 𝑡 ∈ 𝐹 ) ∧ 𝑎 ∈ ∩ ran 𝑈 ) → ¬ 𝑎 ∈ ∪ ran 𝑍 )
38		nelne1	⊢ ( ( 𝑎 ∈ ∪ ran 𝑡 ∧ ¬ 𝑎 ∈ ∪ ran 𝑍 ) → ∪ ran 𝑡 ≠ ∪ ran 𝑍 )
39	27 37 38	syl2an2	⊢ ( ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ∪ ran 𝑡 ∈ 𝐹 ) ∧ 𝑎 ∈ ∩ ran 𝑈 ) → ∪ ran 𝑡 ≠ ∪ ran 𝑍 )
40	39	necomd	⊢ ( ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ∪ ran 𝑡 ∈ 𝐹 ) ∧ 𝑎 ∈ ∩ ran 𝑈 ) → ∪ ran 𝑍 ≠ ∪ ran 𝑡 )
41	13 40	exlimddv	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ∪ ran 𝑡 ∈ 𝐹 ) → ∪ ran 𝑍 ≠ ∪ ran 𝑡 )
42		df-pss	⊢ ( ∪ ran 𝑍 ⊊ ∪ ran 𝑡 ↔ ( ∪ ran 𝑍 ⊆ ∪ ran 𝑡 ∧ ∪ ran 𝑍 ≠ ∪ ran 𝑡 ) )
43	9 41 42	sylanbrc	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ∪ ran 𝑡 ∈ 𝐹 ) → ∪ ran 𝑍 ⊊ ∪ ran 𝑡 )
44	7 43	sylan2	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ ( 𝐺 ∈ 𝐹 ∧ ∪ ran 𝑡 ⊆ 𝐺 ) ) → ∪ ran 𝑍 ⊊ ∪ ran 𝑡 )
45	44	3impb	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ 𝐺 ∈ 𝐹 ∧ ∪ ran 𝑡 ⊆ 𝐺 ) → ∪ ran 𝑍 ⊊ ∪ ran 𝑡 )