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 ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ⟶ 𝑆 ) )