This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fonex

Description: The domain of a surjection is a proper class if the range is a proper class as well. Can be used to prove that if a structure component extractor restricted to a class maps onto a proper class, then the class is a proper class as well. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypotheses fonex.1 ⊢ B ∉ V
fonex.2 ⊢ F : A ⟶ onto B
Assertion fonex ⊢ A ∉ V

Proof

Step Hyp Ref Expression
1 fonex.1 ⊢ B ∉ V
2 fonex.2 ⊢ F : A ⟶ onto B
3 1 neli ⊢ ¬ B ∈ V
4 fofun ⊢ F : A ⟶ onto B → Fun ⁡ F
5 2 4 ax-mp ⊢ Fun ⁡ F
6 funrnex ⊢ dom ⁡ F ∈ V → Fun ⁡ F → ran ⁡ F ∈ V
7 5 6 mpi ⊢ dom ⁡ F ∈ V → ran ⁡ F ∈ V
8 fofn ⊢ F : A ⟶ onto B → F Fn A
9 2 8 ax-mp ⊢ F Fn A
10 9 fndmi ⊢ dom ⁡ F = A
11 10 eleq1i ⊢ dom ⁡ F ∈ V ↔ A ∈ V
12 forn ⊢ F : A ⟶ onto B → ran ⁡ F = B
13 2 12 ax-mp ⊢ ran ⁡ F = B
14 13 eleq1i ⊢ ran ⁡ F ∈ V ↔ B ∈ V
15 7 11 14 3imtr3i ⊢ A ∈ V → B ∈ V
16 3 15 mto ⊢ ¬ A ∈ V
17 16 nelir ⊢ A ∉ V