Theorem 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	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step	Hyp	Ref	Expression
1		r1tr	⊢ Tr ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) )
2		rankidb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
3		trss	⊢ ( Tr ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → 𝐴 ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ) )
4	1 2 3	mpsyl	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
5		rankdmr1	⊢ ( rank ‘ 𝐴 ) ∈ dom 𝑅1
6		r1sucg	⊢ ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
7	5 6	ax-mp	⊢ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) )
8	4 7	sseqtrdi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
9		sspwuni	⊢ ( 𝐴 ⊆ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ↔ ∪ 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
10	8 9	sylib	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
11		fvex	⊢ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∈ V
12	11	elpw2	⊢ ( ∪ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ↔ ∪ 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
13	10 12	sylibr	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
14	13 7	eleqtrrdi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
15		r1elwf	⊢ ( ∪ 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
16	14 15	syl	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
17		pwwf	⊢ ( ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
18		pwuni	⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
19		sswf	⊢ ( ( 𝒫 ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ⊆ 𝒫 ∪ 𝐴 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
20	18 19	mpan2	⊢ ( 𝒫 ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
21	17 20	sylbi	⊢ ( ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
22	16 21	impbii	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )