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

Metamath Proof Explorer

Theorem fconst5

Description: Two ways to express that a function is constant. (Contributed by NM, 27-Nov-2007)

Ref Expression
Assertion fconst5 ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅ ) → ( 𝐹 = ( 𝐴 × { 𝐵 } ) ↔ ran 𝐹 = { 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 rneq ⊢ ( 𝐹 = ( 𝐴 × { 𝐵 } ) → ran 𝐹 = ran ( 𝐴 × { 𝐵 } ) )
2 rnxp ⊢ ( 𝐴 ≠ ∅ → ran ( 𝐴 × { 𝐵 } ) = { 𝐵 } )
3 2 eqeq2d ⊢ ( 𝐴 ≠ ∅ → ( ran 𝐹 = ran ( 𝐴 × { 𝐵 } ) ↔ ran 𝐹 = { 𝐵 } ) )
4 1 3 imbitrid ⊢ ( 𝐴 ≠ ∅ → ( 𝐹 = ( 𝐴 × { 𝐵 } ) → ran 𝐹 = { 𝐵 } ) )
5 4 adantl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅ ) → ( 𝐹 = ( 𝐴 × { 𝐵 } ) → ran 𝐹 = { 𝐵 } ) )
6 df-fo ⊢ ( 𝐹 : 𝐴 –onto→ { 𝐵 } ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = { 𝐵 } ) )
7 fof ⊢ ( 𝐹 : 𝐴 –onto→ { 𝐵 } → 𝐹 : 𝐴 ⟶ { 𝐵 } )
8 6 7 sylbir ⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = { 𝐵 } ) → 𝐹 : 𝐴 ⟶ { 𝐵 } )
9 fconst2g ⊢ ( 𝐵 ∈ V → ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
10 8 9 imbitrid ⊢ ( 𝐵 ∈ V → ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = { 𝐵 } ) → 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
11 10 expd ⊢ ( 𝐵 ∈ V → ( 𝐹 Fn 𝐴 → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) ) )
12 11 adantrd ⊢ ( 𝐵 ∈ V → ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅ ) → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) ) )
13 fnrel ⊢ ( 𝐹 Fn 𝐴 → Rel 𝐹 )
14 snprc ⊢ ( ¬ 𝐵 ∈ V ↔ { 𝐵 } = ∅ )
15 relrn0 ⊢ ( Rel 𝐹 → ( 𝐹 = ∅ ↔ ran 𝐹 = ∅ ) )
16 15 biimprd ⊢ ( Rel 𝐹 → ( ran 𝐹 = ∅ → 𝐹 = ∅ ) )
17 16 adantl ⊢ ( ( { 𝐵 } = ∅ ∧ Rel 𝐹 ) → ( ran 𝐹 = ∅ → 𝐹 = ∅ ) )
18 eqeq2 ⊢ ( { 𝐵 } = ∅ → ( ran 𝐹 = { 𝐵 } ↔ ran 𝐹 = ∅ ) )
19 18 adantr ⊢ ( ( { 𝐵 } = ∅ ∧ Rel 𝐹 ) → ( ran 𝐹 = { 𝐵 } ↔ ran 𝐹 = ∅ ) )
20 xpeq2 ⊢ ( { 𝐵 } = ∅ → ( 𝐴 × { 𝐵 } ) = ( 𝐴 × ∅ ) )
21 xp0 ⊢ ( 𝐴 × ∅ ) = ∅
22 20 21 eqtrdi ⊢ ( { 𝐵 } = ∅ → ( 𝐴 × { 𝐵 } ) = ∅ )
23 22 eqeq2d ⊢ ( { 𝐵 } = ∅ → ( 𝐹 = ( 𝐴 × { 𝐵 } ) ↔ 𝐹 = ∅ ) )
24 23 adantr ⊢ ( ( { 𝐵 } = ∅ ∧ Rel 𝐹 ) → ( 𝐹 = ( 𝐴 × { 𝐵 } ) ↔ 𝐹 = ∅ ) )
25 17 19 24 3imtr4d ⊢ ( ( { 𝐵 } = ∅ ∧ Rel 𝐹 ) → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
26 25 ex ⊢ ( { 𝐵 } = ∅ → ( Rel 𝐹 → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) ) )
27 14 26 sylbi ⊢ ( ¬ 𝐵 ∈ V → ( Rel 𝐹 → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) ) )
28 13 27 syl5 ⊢ ( ¬ 𝐵 ∈ V → ( 𝐹 Fn 𝐴 → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) ) )
29 28 adantrd ⊢ ( ¬ 𝐵 ∈ V → ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅ ) → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) ) )
30 12 29 pm2.61i ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅ ) → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
31 5 30 impbid ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅ ) → ( 𝐹 = ( 𝐴 × { 𝐵 } ) ↔ ran 𝐹 = { 𝐵 } ) )