This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r1elssi

Description: The range of the R1 function is transitive. Lemma 2.10 of Kunen p. 97. One direction of r1elss that doesn't need A to be a set. (Contributed by Mario Carneiro, 22-Mar-2013) (Revised by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	r1elssi	$⊢ A \in ⋃ R_{1} [On] \to A \subseteq ⋃ R_{1} [On]$

Proof

Step	Hyp	Ref	Expression
1		triun	$⊢ \forall x \in On Tr R_{1} (x) \to Tr ⋃_{x \in On} R_{1} (x)$
2		r1tr	$⊢ Tr R_{1} (x)$
3	2	a1i	$⊢ x \in On \to Tr R_{1} (x)$
4	1 3	mprg	$⊢ Tr ⋃_{x \in On} R_{1} (x)$
5		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
6	5	simpli	$⊢ Fun R_{1}$
7		funiunfv	$⊢ Fun R_{1} \to ⋃_{x \in On} R_{1} (x) = ⋃ R_{1} [On]$
8	6 7	ax-mp	$⊢ ⋃_{x \in On} R_{1} (x) = ⋃ R_{1} [On]$
9		treq	$⊢ ⋃_{x \in On} R_{1} (x) = ⋃ R_{1} [On] \to (Tr ⋃_{x \in On} R_{1} (x) \leftrightarrow Tr ⋃ R_{1} [On])$
10	8 9	ax-mp	$⊢ Tr ⋃_{x \in On} R_{1} (x) \leftrightarrow Tr ⋃ R_{1} [On]$
11	4 10	mpbi	$⊢ Tr ⋃ R_{1} [On]$
12		trss	$⊢ Tr ⋃ R_{1} [On] \to (A \in ⋃ R_{1} [On] \to A \subseteq ⋃ R_{1} [On])$
13	11 12	ax-mp	$⊢ A \in ⋃ R_{1} [On] \to A \subseteq ⋃ R_{1} [On]$