wfgru

Description: The wellfounded part of a universe is another universe. (Contributed by Mario Carneiro, 17-Jun-2013)

		Ref	Expression
	Assertion	wfgru	$⊢ U \in Univ \to U \cap ⋃ R_{1} [On] \in Univ$

Proof

Step	Hyp	Ref	Expression
1		dftr3	$⊢ Tr ⋃ R_{1} [On] \leftrightarrow \forall x \in ⋃ R_{1} [On] x \subseteq ⋃ R_{1} [On]$
2		r1elssi	$⊢ x \in ⋃ R_{1} [On] \to x \subseteq ⋃ R_{1} [On]$
3	1 2	mprgbir	$⊢ Tr ⋃ R_{1} [On]$
4		pwwf	$⊢ x \in ⋃ R_{1} [On] \leftrightarrow 𝒫 x \in ⋃ R_{1} [On]$
5	4	biimpi	$⊢ x \in ⋃ R_{1} [On] \to 𝒫 x \in ⋃ R_{1} [On]$
6		prwf	$⊢ (x \in ⋃ R_{1} [On] \land y \in ⋃ R_{1} [On]) \to \{x, y\} \in ⋃ R_{1} [On]$
7	6	ralrimiva	$⊢ x \in ⋃ R_{1} [On] \to \forall y \in ⋃ R_{1} [On] \{x, y\} \in ⋃ R_{1} [On]$
8		frn	$⊢ y : x ⟶ ⋃ R_{1} [On] \to ran y \subseteq ⋃ R_{1} [On]$
9		vex	$⊢ y \in V$
10	9	rnex	$⊢ ran y \in V$
11	10	r1elss	$⊢ ran y \in ⋃ R_{1} [On] \leftrightarrow ran y \subseteq ⋃ R_{1} [On]$
12		uniwf	$⊢ ran y \in ⋃ R_{1} [On] \leftrightarrow ⋃ ran y \in ⋃ R_{1} [On]$
13	11 12	bitr3i	$⊢ ran y \subseteq ⋃ R_{1} [On] \leftrightarrow ⋃ ran y \in ⋃ R_{1} [On]$
14	8 13	sylib	$⊢ y : x ⟶ ⋃ R_{1} [On] \to ⋃ ran y \in ⋃ R_{1} [On]$
15	14	ax-gen	$⊢ \forall y (y : x ⟶ ⋃ R_{1} [On] \to ⋃ ran y \in ⋃ R_{1} [On])$
16	15	a1i	$⊢ x \in ⋃ R_{1} [On] \to \forall y (y : x ⟶ ⋃ R_{1} [On] \to ⋃ ran y \in ⋃ R_{1} [On])$
17	5 7 16	3jca	$⊢ x \in ⋃ R_{1} [On] \to (𝒫 x \in ⋃ R_{1} [On] \land \forall y \in ⋃ R_{1} [On] \{x, y\} \in ⋃ R_{1} [On] \land \forall y (y : x ⟶ ⋃ R_{1} [On] \to ⋃ ran y \in ⋃ R_{1} [On]))$
18	17	rgen	$⊢ \forall x \in ⋃ R_{1} [On] (𝒫 x \in ⋃ R_{1} [On] \land \forall y \in ⋃ R_{1} [On] \{x, y\} \in ⋃ R_{1} [On] \land \forall y (y : x ⟶ ⋃ R_{1} [On] \to ⋃ ran y \in ⋃ R_{1} [On]))$
19		ingru	$⊢ (Tr ⋃ R_{1} [On] \land \forall x \in ⋃ R_{1} [On] (𝒫 x \in ⋃ R_{1} [On] \land \forall y \in ⋃ R_{1} [On] \{x, y\} \in ⋃ R_{1} [On] \land \forall y (y : x ⟶ ⋃ R_{1} [On] \to ⋃ ran y \in ⋃ R_{1} [On]))) \to (U \in Univ \to U \cap ⋃ R_{1} [On] \in Univ)$
20	3 18 19	mp2an	$⊢ U \in Univ \to U \cap ⋃ R_{1} [On] \in Univ$

Metamath Proof Explorer

Theorem wfgru

Proof