unirnfdomd

Description: The union of the range of a function from an infinite set into the class of finite sets is dominated by its domain. Deduction form. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	unirnfdomd.1	$⊢ φ \to F : T ⟶ Fin$
	unirnfdomd.2	$⊢ φ \to \neg T \in Fin$
	unirnfdomd.3	$⊢ φ \to T \in V$
Assertion	unirnfdomd	$⊢ φ \to ⋃ ran F ≼ T$

Proof

Step	Hyp	Ref	Expression
1		unirnfdomd.1	$⊢ φ \to F : T ⟶ Fin$
2		unirnfdomd.2	$⊢ φ \to \neg T \in Fin$
3		unirnfdomd.3	$⊢ φ \to T \in V$
4	1	ffnd	$⊢ φ \to F Fn T$
5		fnex	$⊢ (F Fn T \land T \in V) \to F \in V$
6	4 3 5	syl2anc	$⊢ φ \to F \in V$
7		rnexg	$⊢ F \in V \to ran F \in V$
8	6 7	syl	$⊢ φ \to ran F \in V$
9		frn	$⊢ F : T ⟶ Fin \to ran F \subseteq Fin$
10		dfss3	$⊢ ran F \subseteq Fin \leftrightarrow \forall x \in ran F x \in Fin$
11	9 10	sylib	$⊢ F : T ⟶ Fin \to \forall x \in ran F x \in Fin$
12		fict	$⊢ x \in Fin \to x ≼ ω$
13	12	ralimi	$⊢ \forall x \in ran F x \in Fin \to \forall x \in ran F x ≼ ω$
14	1 11 13	3syl	$⊢ φ \to \forall x \in ran F x ≼ ω$
15		unidom	$⊢ (ran F \in V \land \forall x \in ran F x ≼ ω) \to ⋃ ran F ≼ (ran F \times ω)$
16	8 14 15	syl2anc	$⊢ φ \to ⋃ ran F ≼ (ran F \times ω)$
17		fnrndomg	$⊢ T \in V \to (F Fn T \to ran F ≼ T)$
18	3 4 17	sylc	$⊢ φ \to ran F ≼ T$
19		omex	$⊢ ω \in V$
20	19	xpdom1	$⊢ ran F ≼ T \to (ran F \times ω) ≼ (T \times ω)$
21	18 20	syl	$⊢ φ \to (ran F \times ω) ≼ (T \times ω)$
22		domtr	$⊢ (⋃ ran F ≼ (ran F \times ω) \land (ran F \times ω) ≼ (T \times ω)) \to ⋃ ran F ≼ (T \times ω)$
23	16 21 22	syl2anc	$⊢ φ \to ⋃ ran F ≼ (T \times ω)$
24		infinf	$⊢ T \in V \to (\neg T \in Fin \leftrightarrow ω ≼ T)$
25	3 24	syl	$⊢ φ \to (\neg T \in Fin \leftrightarrow ω ≼ T)$
26	2 25	mpbid	$⊢ φ \to ω ≼ T$
27		xpdom2g	$⊢ (T \in V \land ω ≼ T) \to (T \times ω) ≼ (T \times T)$
28	3 26 27	syl2anc	$⊢ φ \to (T \times ω) ≼ (T \times T)$
29		domtr	$⊢ (⋃ ran F ≼ (T \times ω) \land (T \times ω) ≼ (T \times T)) \to ⋃ ran F ≼ (T \times T)$
30	23 28 29	syl2anc	$⊢ φ \to ⋃ ran F ≼ (T \times T)$
31		infxpidm	$⊢ ω ≼ T \to (T \times T) \approx T$
32	26 31	syl	$⊢ φ \to (T \times T) \approx T$
33		domentr	$⊢ (⋃ ran F ≼ (T \times T) \land (T \times T) \approx T) \to ⋃ ran F ≼ T$
34	30 32 33	syl2anc	$⊢ φ \to ⋃ ran F ≼ T$

Metamath Proof Explorer

Theorem unirnfdomd

Proof