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 F = ran x X A B
flift.2 φ x X A R
flift.3 φ x X B S
Assertion fliftf φ Fun F F : ran x X A S

Proof

Step Hyp Ref Expression
1 flift.1 F = ran x X A B
2 flift.2 φ x X A R
3 flift.3 φ x X B S
4 simpr φ Fun F Fun F
5 1 2 3 fliftel φ y F z x X y = A z = B
6 5 exbidv φ z y F z z x X y = A z = B
7 6 adantr φ Fun F z y F z z x X y = A z = B
8 rexcom4 x X z y = A z = B z x X y = A z = B
9 19.42v z y = A z = B y = A z z = B
10 elisset B S z z = B
11 3 10 syl φ x X z z = B
12 11 biantrud φ x X y = A y = A z z = B
13 9 12 bitr4id φ x X z y = A z = B y = A
14 13 rexbidva φ x X z y = A z = B x X y = A
15 14 adantr φ Fun F x X z y = A z = B x X y = A
16 8 15 bitr3id φ Fun F z x X y = A z = B x X y = A
17 7 16 bitrd φ Fun F z y F z x X y = A
18 17 abbidv φ Fun F y | z y F z = y | x X y = A
19 df-dm dom F = y | z y F z
20 eqid x X A = x X A
21 20 rnmpt ran x X A = y | x X y = A
22 18 19 21 3eqtr4g φ Fun F dom F = ran x X A
23 df-fn F Fn ran x X A Fun F dom F = ran x X A
24 4 22 23 sylanbrc φ Fun F F Fn ran x X A
25 1 2 3 fliftrel φ F R × S
26 25 adantr φ Fun F F R × S
27 rnss F R × S ran F ran R × S
28 26 27 syl φ Fun F ran F ran R × S
29 rnxpss ran R × S S
30 28 29 sstrdi φ Fun F ran F S
31 df-f F : ran x X A S F Fn ran x X A ran F S
32 24 30 31 sylanbrc φ Fun F F : ran x X A S
33 32 ex φ Fun F F : ran x X A S
34 ffun F : ran x X A S Fun F
35 33 34 impbid1 φ Fun F F : ran x X A S