tskurn

Description: A transitive Tarski class is closed under small unions. (Contributed by Mario Carneiro, 22-Jun-2013)

		Ref	Expression
	Assertion	tskurn	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to ⋃ ran F \in T$

Proof

Step	Hyp	Ref	Expression
1		simp1l	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to T \in Tarski$
2		simp1r	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to Tr T$
3		frn	$⊢ F : A ⟶ T \to ran F \subseteq T$
4	3	3ad2ant3	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to ran F \subseteq T$
5		tskwe2	$⊢ T \in Tarski \to T \in dom card$
6	1 5	syl	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to T \in dom card$
7		simp2	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to A \in T$
8		trss	$⊢ Tr T \to (A \in T \to A \subseteq T)$
9	2 7 8	sylc	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to A \subseteq T$
10		ssnum	$⊢ (T \in dom card \land A \subseteq T) \to A \in dom card$
11	6 9 10	syl2anc	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to A \in dom card$
12		ffn	$⊢ F : A ⟶ T \to F Fn A$
13		dffn4	$⊢ F Fn A \leftrightarrow F : A \underset{onto}{⟶} ran F$
14	12 13	sylib	$⊢ F : A ⟶ T \to F : A \underset{onto}{⟶} ran F$
15	14	3ad2ant3	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to F : A \underset{onto}{⟶} ran F$
16		fodomnum	$⊢ A \in dom card \to (F : A \underset{onto}{⟶} ran F \to ran F ≼ A)$
17	11 15 16	sylc	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to ran F ≼ A$
18		tsksdom	$⊢ (T \in Tarski \land A \in T) \to A ≺ T$
19	1 7 18	syl2anc	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to A ≺ T$
20		domsdomtr	$⊢ (ran F ≼ A \land A ≺ T) \to ran F ≺ T$
21	17 19 20	syl2anc	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to ran F ≺ T$
22		tskssel	$⊢ (T \in Tarski \land ran F \subseteq T \land ran F ≺ T) \to ran F \in T$
23	1 4 21 22	syl3anc	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to ran F \in T$
24		tskuni	$⊢ (T \in Tarski \land Tr T \land ran F \in T) \to ⋃ ran F \in T$
25	1 2 23 24	syl3anc	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land F : A ⟶ T) \to ⋃ ran F \in T$

Metamath Proof Explorer

Theorem tskurn

Proof