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 ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∉ V ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V )

Proof

Step Hyp Ref Expression
1 abanssl ⊢ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ⊆ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 }
2 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐴 )
3 vex ⊢ 𝑦 ∈ V
4 3 a1i ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝑦 ∈ V )
5 fsetsnprcnex ⊢ ( ( 𝑦 ∈ V ∧ 𝐵 ∉ V ) → { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ∉ V )
6 4 5 sylan ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐵 ∉ V ) → { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ∉ V )
7 df-nel ⊢ ( { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ∉ V ↔ ¬ { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ∈ V )
8 6 7 sylib ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐵 ∉ V ) → ¬ { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ∈ V )
9 eqid ⊢ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } = { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) }
10 eqid ⊢ { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } = { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 }
11 eqid ⊢ ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ) = ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) )
12 9 10 11 cfsetsnfsetf1o ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ) : { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } –1-1-onto→ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } )
13 12 ancoms ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ) : { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } –1-1-onto→ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } )
14 13 adantr ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐵 ∉ V ) → ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ) : { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } –1-1-onto→ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } )
15 f1ovv ⊢ ( ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ) : { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } –1-1-onto→ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } → ( { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ∈ V ↔ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ∈ V ) )
16 15 bicomd ⊢ ( ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ) : { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } –1-1-onto→ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } → ( { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ∈ V ↔ { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ∈ V ) )
17 14 16 syl ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐵 ∉ V ) → ( { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ∈ V ↔ { 𝑓 ∣ 𝑓 : { 𝑦 } ⟶ 𝐵 } ∈ V ) )
18 8 17 mtbird ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐵 ∉ V ) → ¬ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ∈ V )
19 18 exp31 ⊢ ( 𝑦 ∈ 𝐴 → ( 𝐴 ∈ 𝑉 → ( 𝐵 ∉ V → ¬ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ∈ V ) ) )
20 19 exlimiv ⊢ ( ∃ 𝑦 𝑦 ∈ 𝐴 → ( 𝐴 ∈ 𝑉 → ( 𝐵 ∉ V → ¬ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ∈ V ) ) )
21 2 20 sylbi ⊢ ( 𝐴 ≠ ∅ → ( 𝐴 ∈ 𝑉 → ( 𝐵 ∉ V → ¬ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ∈ V ) ) )
22 21 impcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( 𝐵 ∉ V → ¬ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ∈ V ) )
23 22 imp ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∉ V ) → ¬ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ∈ V )
24 df-nel ⊢ ( { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ∉ V ↔ ¬ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ∈ V )
25 23 24 sylibr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∉ V ) → { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ∉ V )
26 prcssprc ⊢ ( ( { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ⊆ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∧ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ∉ V ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V )
27 1 25 26 sylancr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∉ V ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V )