Metamath Proof Explorer

Theorem fsetprcnexALT

Description: First version of proof for fsetprcnex , which was much more complicated. (Contributed by AV, 14-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion fsetprcnexALT ⊢ A ∈ V ∧ A ≠ ∅ ∧ B ∉ V → f | f : A ⟶ B ∉ V

Proof

Step Hyp Ref Expression
1 abanssl ⊢ f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ⊆ f | f : A ⟶ B
2 n0 ⊢ A ≠ ∅ ↔ ∃ y y ∈ A
3 vex ⊢ y ∈ V
4 3 a1i ⊢ y ∈ A ∧ A ∈ V → y ∈ V
5 fsetsnprcnex ⊢ y ∈ V ∧ B ∉ V → f | f : y ⟶ B ∉ V
6 4 5 sylan ⊢ y ∈ A ∧ A ∈ V ∧ B ∉ V → f | f : y ⟶ B ∉ V
7 df-nel ⊢ f | f : y ⟶ B ∉ V ↔ ¬ f | f : y ⟶ B ∈ V
8 6 7 sylib ⊢ y ∈ A ∧ A ∈ V ∧ B ∉ V → ¬ f | f : y ⟶ B ∈ V
9 eqid ⊢ f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b = f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b
10 eqid ⊢ f | f : y ⟶ B = f | f : y ⟶ B
11 eqid ⊢ g ∈ f | f : y ⟶ B ⟼ a ∈ A ⟼ g ⁡ y = g ∈ f | f : y ⟶ B ⟼ a ∈ A ⟼ g ⁡ y
12 9 10 11 cfsetsnfsetf1o ⊢ A ∈ V ∧ y ∈ A → g ∈ f | f : y ⟶ B ⟼ a ∈ A ⟼ g ⁡ y : f | f : y ⟶ B ⟶ 1-1 onto f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b
13 12 ancoms ⊢ y ∈ A ∧ A ∈ V → g ∈ f | f : y ⟶ B ⟼ a ∈ A ⟼ g ⁡ y : f | f : y ⟶ B ⟶ 1-1 onto f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b
14 13 adantr ⊢ y ∈ A ∧ A ∈ V ∧ B ∉ V → g ∈ f | f : y ⟶ B ⟼ a ∈ A ⟼ g ⁡ y : f | f : y ⟶ B ⟶ 1-1 onto f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b
15 f1ovv ⊢ g ∈ f | f : y ⟶ B ⟼ a ∈ A ⟼ g ⁡ y : f | f : y ⟶ B ⟶ 1-1 onto f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b → f | f : y ⟶ B ∈ V ↔ f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ∈ V
16 15 bicomd ⊢ g ∈ f | f : y ⟶ B ⟼ a ∈ A ⟼ g ⁡ y : f | f : y ⟶ B ⟶ 1-1 onto f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b → f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ∈ V ↔ f | f : y ⟶ B ∈ V
17 14 16 syl ⊢ y ∈ A ∧ A ∈ V ∧ B ∉ V → f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ∈ V ↔ f | f : y ⟶ B ∈ V
18 8 17 mtbird ⊢ y ∈ A ∧ A ∈ V ∧ B ∉ V → ¬ f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ∈ V
19 18 exp31 ⊢ y ∈ A → A ∈ V → B ∉ V → ¬ f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ∈ V
20 19 exlimiv ⊢ ∃ y y ∈ A → A ∈ V → B ∉ V → ¬ f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ∈ V
21 2 20 sylbi ⊢ A ≠ ∅ → A ∈ V → B ∉ V → ¬ f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ∈ V
22 21 impcom ⊢ A ∈ V ∧ A ≠ ∅ → B ∉ V → ¬ f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ∈ V
23 22 imp ⊢ A ∈ V ∧ A ≠ ∅ ∧ B ∉ V → ¬ f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ∈ V
24 df-nel ⊢ f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ∉ V ↔ ¬ f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ∈ V
25 23 24 sylibr ⊢ A ∈ V ∧ A ≠ ∅ ∧ B ∉ V → f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ∉ V
26 prcssprc ⊢ f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ⊆ f | f : A ⟶ B ∧ f | f : A ⟶ B ∧ ∃ b ∈ B ∀ z ∈ A f ⁡ z = b ∉ V → f | f : A ⟶ B ∉ V
27 1 25 26 sylancr ⊢ A ∈ V ∧ A ≠ ∅ ∧ B ∉ V → f | f : A ⟶ B ∉ V