Theorem elwf

Description: An element of a well-founded set is well-founded. (Contributed by BTernaryTau, 30-Dec-2025)

	Ref	Expression
Assertion	elwf	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step	Hyp	Ref	Expression
1		elssuni	⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝐴 )
2		uniwf	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
3		sswf	⊢ ( ( ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ⊆ ∪ 𝐴 ) → 𝐵 ∈ ∪ ( 𝑅1 “ On ) )
4	2 3	sylanb	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ⊆ ∪ 𝐴 ) → 𝐵 ∈ ∪ ( 𝑅1 “ On ) )
5	1 4	sylan2	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ ∪ ( 𝑅1 “ On ) )