uniwf

Description: A union is well-founded iff the base set is. (Contributed by Mario Carneiro, 8-Jun-2013) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	uniwf	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow ⋃ A \in ⋃ R_{1} [On]$

Proof

Step	Hyp	Ref	Expression
1		r1tr	$⊢ Tr R_{1} (suc rank (A))$
2		rankidb	$⊢ A \in ⋃ R_{1} [On] \to A \in R_{1} (suc rank (A))$
3		trss	$⊢ Tr R_{1} (suc rank (A)) \to (A \in R_{1} (suc rank (A)) \to A \subseteq R_{1} (suc rank (A)))$
4	1 2 3	mpsyl	$⊢ A \in ⋃ R_{1} [On] \to A \subseteq R_{1} (suc rank (A))$
5		rankdmr1	$⊢ rank (A) \in dom R_{1}$
6		r1sucg	$⊢ rank (A) \in dom R_{1} \to R_{1} (suc rank (A)) = 𝒫 R_{1} (rank (A))$
7	5 6	ax-mp	$⊢ R_{1} (suc rank (A)) = 𝒫 R_{1} (rank (A))$
8	4 7	sseqtrdi	$⊢ A \in ⋃ R_{1} [On] \to A \subseteq 𝒫 R_{1} (rank (A))$
9		sspwuni	$⊢ A \subseteq 𝒫 R_{1} (rank (A)) \leftrightarrow ⋃ A \subseteq R_{1} (rank (A))$
10	8 9	sylib	$⊢ A \in ⋃ R_{1} [On] \to ⋃ A \subseteq R_{1} (rank (A))$
11		fvex	$⊢ R_{1} (rank (A)) \in V$
12	11	elpw2	$⊢ ⋃ A \in 𝒫 R_{1} (rank (A)) \leftrightarrow ⋃ A \subseteq R_{1} (rank (A))$
13	10 12	sylibr	$⊢ A \in ⋃ R_{1} [On] \to ⋃ A \in 𝒫 R_{1} (rank (A))$
14	13 7	eleqtrrdi	$⊢ A \in ⋃ R_{1} [On] \to ⋃ A \in R_{1} (suc rank (A))$
15		r1elwf	$⊢ ⋃ A \in R_{1} (suc rank (A)) \to ⋃ A \in ⋃ R_{1} [On]$
16	14 15	syl	$⊢ A \in ⋃ R_{1} [On] \to ⋃ A \in ⋃ R_{1} [On]$
17		pwwf	$⊢ ⋃ A \in ⋃ R_{1} [On] \leftrightarrow 𝒫 ⋃ A \in ⋃ R_{1} [On]$
18		pwuni	$⊢ A \subseteq 𝒫 ⋃ A$
19		sswf	$⊢ (𝒫 ⋃ A \in ⋃ R_{1} [On] \land A \subseteq 𝒫 ⋃ A) \to A \in ⋃ R_{1} [On]$
20	18 19	mpan2	$⊢ 𝒫 ⋃ A \in ⋃ R_{1} [On] \to A \in ⋃ R_{1} [On]$
21	17 20	sylbi	$⊢ ⋃ A \in ⋃ R_{1} [On] \to A \in ⋃ R_{1} [On]$
22	16 21	impbii	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow ⋃ A \in ⋃ R_{1} [On]$

Metamath Proof Explorer

Theorem uniwf

Proof