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

Metamath Proof Explorer

Theorem fliftf

Description: The domain and range of the function F . (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses flift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
flift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
flift.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
Assertion fliftf ( 𝜑 → ( Fun 𝐹 ↔ 𝐹 : ran ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ⟶ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 flift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
2 flift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
3 flift.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
4 simpr ⊢ ( ( 𝜑 ∧ Fun 𝐹 ) → Fun 𝐹 )
5 1 2 3 fliftel ⊢ ( 𝜑 → ( 𝑦 𝐹 𝑧 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) ) )
6 5 exbidv ⊢ ( 𝜑 → ( ∃ 𝑧 𝑦 𝐹 𝑧 ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝑋 ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) ) )
7 6 adantr ⊢ ( ( 𝜑 ∧ Fun 𝐹 ) → ( ∃ 𝑧 𝑦 𝐹 𝑧 ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝑋 ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) ) )
8 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑧 ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝑋 ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) )
9 19.42v ⊢ ( ∃ 𝑧 ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) ↔ ( 𝑦 = 𝐴 ∧ ∃ 𝑧 𝑧 = 𝐵 ) )
10 elisset ⊢ ( 𝐵 ∈ 𝑆 → ∃ 𝑧 𝑧 = 𝐵 )
11 3 10 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑧 𝑧 = 𝐵 )
12 11 biantrud ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 = 𝐴 ↔ ( 𝑦 = 𝐴 ∧ ∃ 𝑧 𝑧 = 𝐵 ) ) )
13 9 12 bitr4id ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑧 ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) ↔ 𝑦 = 𝐴 ) )
14 13 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑧 ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) ↔ ∃ 𝑥 ∈ 𝑋 𝑦 = 𝐴 ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ Fun 𝐹 ) → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑧 ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) ↔ ∃ 𝑥 ∈ 𝑋 𝑦 = 𝐴 ) )
16 8 15 bitr3id ⊢ ( ( 𝜑 ∧ Fun 𝐹 ) → ( ∃ 𝑧 ∃ 𝑥 ∈ 𝑋 ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) ↔ ∃ 𝑥 ∈ 𝑋 𝑦 = 𝐴 ) )
17 7 16 bitrd ⊢ ( ( 𝜑 ∧ Fun 𝐹 ) → ( ∃ 𝑧 𝑦 𝐹 𝑧 ↔ ∃ 𝑥 ∈ 𝑋 𝑦 = 𝐴 ) )
18 17 abbidv ⊢ ( ( 𝜑 ∧ Fun 𝐹 ) → { 𝑦 ∣ ∃ 𝑧 𝑦 𝐹 𝑧 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 = 𝐴 } )
19 df-dm ⊢ dom 𝐹 = { 𝑦 ∣ ∃ 𝑧 𝑦 𝐹 𝑧 }
20 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
21 20 rnmpt ⊢ ran ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 = 𝐴 }
22 18 19 21 3eqtr4g ⊢ ( ( 𝜑 ∧ Fun 𝐹 ) → dom 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
23 df-fn ⊢ ( 𝐹 Fn ran ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↔ ( Fun 𝐹 ∧ dom 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) )
24 4 22 23 sylanbrc ⊢ ( ( 𝜑 ∧ Fun 𝐹 ) → 𝐹 Fn ran ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
25 1 2 3 fliftrel ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑅 × 𝑆 ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ Fun 𝐹 ) → 𝐹 ⊆ ( 𝑅 × 𝑆 ) )
27 rnss ⊢ ( 𝐹 ⊆ ( 𝑅 × 𝑆 ) → ran 𝐹 ⊆ ran ( 𝑅 × 𝑆 ) )
28 26 27 syl ⊢ ( ( 𝜑 ∧ Fun 𝐹 ) → ran 𝐹 ⊆ ran ( 𝑅 × 𝑆 ) )
29 rnxpss ⊢ ran ( 𝑅 × 𝑆 ) ⊆ 𝑆
30 28 29 sstrdi ⊢ ( ( 𝜑 ∧ Fun 𝐹 ) → ran 𝐹 ⊆ 𝑆 )
31 df-f ⊢ ( 𝐹 : ran ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ⟶ 𝑆 ↔ ( 𝐹 Fn ran ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∧ ran 𝐹 ⊆ 𝑆 ) )
32 24 30 31 sylanbrc ⊢ ( ( 𝜑 ∧ Fun 𝐹 ) → 𝐹 : ran ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ⟶ 𝑆 )
33 32 ex ⊢ ( 𝜑 → ( Fun 𝐹 → 𝐹 : ran ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ⟶ 𝑆 ) )
34 ffun ⊢ ( 𝐹 : ran ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ⟶ 𝑆 → Fun 𝐹 )
35 33 34 impbid1 ⊢ ( 𝜑 → ( Fun 𝐹 ↔ 𝐹 : ran ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ⟶ 𝑆 ) )