Theorem mnurnd

Description: Minimal universes contain ranges of functions from an element of the universe to the universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnurnd.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
	mnurnd.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
	mnurnd.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	mnurnd.4	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑈 )
Assertion	mnurnd	⊢ ( 𝜑 → ran 𝐹 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		mnurnd.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
2		mnurnd.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
3		mnurnd.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
4		mnurnd.4	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑈 )
5	3	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
6	5	iftrued	⊢ ( 𝜑 → if ( 𝐴 ∈ V , 𝐴 , ∅ ) = 𝐴 )
7	6 3	eqeltrd	⊢ ( 𝜑 → if ( 𝐴 ∈ V , 𝐴 , ∅ ) ∈ 𝑈 )
8	6	feq2d	⊢ ( 𝜑 → ( 𝐹 : if ( 𝐴 ∈ V , 𝐴 , ∅ ) ⟶ 𝑈 ↔ 𝐹 : 𝐴 ⟶ 𝑈 ) )
9	4 8	mpbird	⊢ ( 𝜑 → 𝐹 : if ( 𝐴 ∈ V , 𝐴 , ∅ ) ⟶ 𝑈 )
10		0ex	⊢ ∅ ∈ V
11	10	elimel	⊢ if ( 𝐴 ∈ V , 𝐴 , ∅ ) ∈ V
12	1 2 7 9 11	mnurndlem2	⊢ ( 𝜑 → ran 𝐹 ∈ 𝑈 )