Theorem fin23lem21

Description: Lemma for fin23 . X is not empty. We only need here that t has at least one set in its range besides (/) ; the much stronger hypothesis here will serve as our induction hypothesis though. (Contributed by Stefan O'Rear, 1-Nov-2014) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	fin23lem.a	⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
	fin23lem17.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
Assertion	fin23lem21	⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ∩ ran 𝑈 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		fin23lem.a	⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
2		fin23lem17.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
3	1 2	fin23lem17	⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ∩ ran 𝑈 ∈ ran 𝑈 )
4	1	fnseqom	⊢ 𝑈 Fn ω
5		fvelrnb	⊢ ( 𝑈 Fn ω → ( ∩ ran 𝑈 ∈ ran 𝑈 ↔ ∃ 𝑎 ∈ ω ( 𝑈 ‘ 𝑎 ) = ∩ ran 𝑈 ) )
6	4 5	ax-mp	⊢ ( ∩ ran 𝑈 ∈ ran 𝑈 ↔ ∃ 𝑎 ∈ ω ( 𝑈 ‘ 𝑎 ) = ∩ ran 𝑈 )
7		id	⊢ ( 𝑎 ∈ ω → 𝑎 ∈ ω )
8		vex	⊢ 𝑡 ∈ V
9		f1f1orn	⊢ ( 𝑡 : ω –1-1→ 𝑉 → 𝑡 : ω –1-1-onto→ ran 𝑡 )
10		f1oen3g	⊢ ( ( 𝑡 ∈ V ∧ 𝑡 : ω –1-1-onto→ ran 𝑡 ) → ω ≈ ran 𝑡 )
11	8 9 10	sylancr	⊢ ( 𝑡 : ω –1-1→ 𝑉 → ω ≈ ran 𝑡 )
12		ominf	⊢ ¬ ω ∈ Fin
13		ssdif0	⊢ ( ran 𝑡 ⊆ { ∅ } ↔ ( ran 𝑡 ∖ { ∅ } ) = ∅ )
14		snfi	⊢ { ∅ } ∈ Fin
15		ssfi	⊢ ( ( { ∅ } ∈ Fin ∧ ran 𝑡 ⊆ { ∅ } ) → ran 𝑡 ∈ Fin )
16	14 15	mpan	⊢ ( ran 𝑡 ⊆ { ∅ } → ran 𝑡 ∈ Fin )
17		enfi	⊢ ( ω ≈ ran 𝑡 → ( ω ∈ Fin ↔ ran 𝑡 ∈ Fin ) )
18	16 17	imbitrrid	⊢ ( ω ≈ ran 𝑡 → ( ran 𝑡 ⊆ { ∅ } → ω ∈ Fin ) )
19	13 18	biimtrrid	⊢ ( ω ≈ ran 𝑡 → ( ( ran 𝑡 ∖ { ∅ } ) = ∅ → ω ∈ Fin ) )
20	19	necon3bd	⊢ ( ω ≈ ran 𝑡 → ( ¬ ω ∈ Fin → ( ran 𝑡 ∖ { ∅ } ) ≠ ∅ ) )
21	11 12 20	mpisyl	⊢ ( 𝑡 : ω –1-1→ 𝑉 → ( ran 𝑡 ∖ { ∅ } ) ≠ ∅ )
22		n0	⊢ ( ( ran 𝑡 ∖ { ∅ } ) ≠ ∅ ↔ ∃ 𝑎 𝑎 ∈ ( ran 𝑡 ∖ { ∅ } ) )
23		eldifsn	⊢ ( 𝑎 ∈ ( ran 𝑡 ∖ { ∅ } ) ↔ ( 𝑎 ∈ ran 𝑡 ∧ 𝑎 ≠ ∅ ) )
24		elssuni	⊢ ( 𝑎 ∈ ran 𝑡 → 𝑎 ⊆ ∪ ran 𝑡 )
25		ssn0	⊢ ( ( 𝑎 ⊆ ∪ ran 𝑡 ∧ 𝑎 ≠ ∅ ) → ∪ ran 𝑡 ≠ ∅ )
26	24 25	sylan	⊢ ( ( 𝑎 ∈ ran 𝑡 ∧ 𝑎 ≠ ∅ ) → ∪ ran 𝑡 ≠ ∅ )
27	23 26	sylbi	⊢ ( 𝑎 ∈ ( ran 𝑡 ∖ { ∅ } ) → ∪ ran 𝑡 ≠ ∅ )
28	27	exlimiv	⊢ ( ∃ 𝑎 𝑎 ∈ ( ran 𝑡 ∖ { ∅ } ) → ∪ ran 𝑡 ≠ ∅ )
29	22 28	sylbi	⊢ ( ( ran 𝑡 ∖ { ∅ } ) ≠ ∅ → ∪ ran 𝑡 ≠ ∅ )
30	21 29	syl	⊢ ( 𝑡 : ω –1-1→ 𝑉 → ∪ ran 𝑡 ≠ ∅ )
31	1	fin23lem14	⊢ ( ( 𝑎 ∈ ω ∧ ∪ ran 𝑡 ≠ ∅ ) → ( 𝑈 ‘ 𝑎 ) ≠ ∅ )
32	7 30 31	syl2anr	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ 𝑎 ∈ ω ) → ( 𝑈 ‘ 𝑎 ) ≠ ∅ )
33		neeq1	⊢ ( ( 𝑈 ‘ 𝑎 ) = ∩ ran 𝑈 → ( ( 𝑈 ‘ 𝑎 ) ≠ ∅ ↔ ∩ ran 𝑈 ≠ ∅ ) )
34	32 33	syl5ibcom	⊢ ( ( 𝑡 : ω –1-1→ 𝑉 ∧ 𝑎 ∈ ω ) → ( ( 𝑈 ‘ 𝑎 ) = ∩ ran 𝑈 → ∩ ran 𝑈 ≠ ∅ ) )
35	34	rexlimdva	⊢ ( 𝑡 : ω –1-1→ 𝑉 → ( ∃ 𝑎 ∈ ω ( 𝑈 ‘ 𝑎 ) = ∩ ran 𝑈 → ∩ ran 𝑈 ≠ ∅ ) )
36	6 35	biimtrid	⊢ ( 𝑡 : ω –1-1→ 𝑉 → ( ∩ ran 𝑈 ∈ ran 𝑈 → ∩ ran 𝑈 ≠ ∅ ) )
37	36	adantl	⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ( ∩ ran 𝑈 ∈ ran 𝑈 → ∩ ran 𝑈 ≠ ∅ ) )
38	3 37	mpd	⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ∩ ran 𝑈 ≠ ∅ )