Metamath Proof Explorer

Theorem fliftfun

Description: The function F is the unique function defined by FA = B , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses flift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
flift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
flift.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
fliftfun.4 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐶 )
fliftfun.5 ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐷 )
Assertion fliftfun ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 flift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
2 flift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
3 flift.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
4 fliftfun.4 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐶 )
5 fliftfun.5 ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐷 )
6 nfv ⊢ Ⅎ 𝑥 𝜑
7 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
8 7 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
9 1 8 nfcxfr ⊢ Ⅎ 𝑥 𝐹
10 9 nffun ⊢ Ⅎ 𝑥 Fun 𝐹
11 fveq2 ⊢ ( 𝐴 = 𝐶 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) )
12 simplr ⊢ ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → Fun 𝐹 )
13 1 2 3 fliftel1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 𝐹 𝐵 )
14 13 ad2ant2r ⊢ ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐴 𝐹 𝐵 )
15 funbrfv ⊢ ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 → ( 𝐹 ‘ 𝐴 ) = 𝐵 ) )
16 12 14 15 sylc ⊢ ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) = 𝐵 )
17 simprr ⊢ ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
18 eqidd ⊢ ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐶 = 𝐶 )
19 eqidd ⊢ ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐷 = 𝐷 )
20 4 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐶 = 𝐴 ↔ 𝐶 = 𝐶 ) )
21 5 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐷 = 𝐵 ↔ 𝐷 = 𝐷 ) )
22 20 21 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ↔ ( 𝐶 = 𝐶 ∧ 𝐷 = 𝐷 ) ) )
23 22 rspcev ⊢ ( ( 𝑦 ∈ 𝑋 ∧ ( 𝐶 = 𝐶 ∧ 𝐷 = 𝐷 ) ) → ∃ 𝑥 ∈ 𝑋 ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) )
24 17 18 19 23 syl12anc ⊢ ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ∃ 𝑥 ∈ 𝑋 ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) )
25 1 2 3 fliftel ⊢ ( 𝜑 → ( 𝐶 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ) )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐶 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ) )
27 24 26 mpbird ⊢ ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐶 𝐹 𝐷 )
28 funbrfv ⊢ ( Fun 𝐹 → ( 𝐶 𝐹 𝐷 → ( 𝐹 ‘ 𝐶 ) = 𝐷 ) )
29 12 27 28 sylc ⊢ ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐶 ) = 𝐷 )
30 16 29 eqeq12d ⊢ ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ↔ 𝐵 = 𝐷 ) )
31 11 30 syl5ib ⊢ ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) )
32 31 anassrs ⊢ ( ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) )
33 32 ralrimiva ⊢ ( ( ( 𝜑 ∧ Fun 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) )
34 33 exp31 ⊢ ( 𝜑 → ( Fun 𝐹 → ( 𝑥 ∈ 𝑋 → ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ) ) )
35 6 10 34 ralrimd ⊢ ( 𝜑 → ( Fun 𝐹 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ) )
36 1 2 3 fliftel ⊢ ( 𝜑 → ( 𝑧 𝐹 𝑢 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ) )
37 1 2 3 fliftel ⊢ ( 𝜑 → ( 𝑧 𝐹 𝑣 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝑧 = 𝐴 ∧ 𝑣 = 𝐵 ) ) )
38 4 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐶 ) )
39 5 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑣 = 𝐵 ↔ 𝑣 = 𝐷 ) )
40 38 39 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑧 = 𝐴 ∧ 𝑣 = 𝐵 ) ↔ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) )
41 40 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝑋 ( 𝑧 = 𝐴 ∧ 𝑣 = 𝐵 ) ↔ ∃ 𝑦 ∈ 𝑋 ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) )
42 37 41 bitrdi ⊢ ( 𝜑 → ( 𝑧 𝐹 𝑣 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) )
43 36 42 anbi12d ⊢ ( 𝜑 → ( ( 𝑧 𝐹 𝑢 ∧ 𝑧 𝐹 𝑣 ) ↔ ( ∃ 𝑥 ∈ 𝑋 ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) )
44 43 biimpd ⊢ ( 𝜑 → ( ( 𝑧 𝐹 𝑢 ∧ 𝑧 𝐹 𝑣 ) → ( ∃ 𝑥 ∈ 𝑋 ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) )
45 reeanv ⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ↔ ( ∃ 𝑥 ∈ 𝑋 ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) )
46 r19.29 ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) → ∃ 𝑥 ∈ 𝑋 ( ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) )
47 r19.29 ⊢ ( ( ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ∧ ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) )
48 eqtr2 ⊢ ( ( 𝑧 = 𝐴 ∧ 𝑧 = 𝐶 ) → 𝐴 = 𝐶 )
49 48 ad2ant2r ⊢ ( ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) → 𝐴 = 𝐶 )
50 49 imim1i ⊢ ( ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) → ( ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) → 𝐵 = 𝐷 ) )
51 50 imp ⊢ ( ( ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ∧ ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) → 𝐵 = 𝐷 )
52 simprlr ⊢ ( ( ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ∧ ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) → 𝑢 = 𝐵 )
53 simprrr ⊢ ( ( ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ∧ ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) → 𝑣 = 𝐷 )
54 51 52 53 3eqtr4d ⊢ ( ( ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ∧ ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) → 𝑢 = 𝑣 )
55 54 rexlimivw ⊢ ( ∃ 𝑦 ∈ 𝑋 ( ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ∧ ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) → 𝑢 = 𝑣 )
56 47 55 syl ⊢ ( ( ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) → 𝑢 = 𝑣 )
57 56 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝑋 ( ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) → 𝑢 = 𝑣 )
58 46 57 syl ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) ) → 𝑢 = 𝑣 )
59 58 ex ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) → 𝑢 = 𝑣 ) )
60 45 59 syl5bir ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) → ( ( ∃ 𝑥 ∈ 𝑋 ( 𝑧 = 𝐴 ∧ 𝑢 = 𝐵 ) ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑧 = 𝐶 ∧ 𝑣 = 𝐷 ) ) → 𝑢 = 𝑣 ) )
61 44 60 syl9 ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) → ( ( 𝑧 𝐹 𝑢 ∧ 𝑧 𝐹 𝑣 ) → 𝑢 = 𝑣 ) ) )
62 61 alrimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) → ∀ 𝑣 ( ( 𝑧 𝐹 𝑢 ∧ 𝑧 𝐹 𝑣 ) → 𝑢 = 𝑣 ) ) )
63 62 alrimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) → ∀ 𝑢 ∀ 𝑣 ( ( 𝑧 𝐹 𝑢 ∧ 𝑧 𝐹 𝑣 ) → 𝑢 = 𝑣 ) ) )
64 63 alrimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) → ∀ 𝑧 ∀ 𝑢 ∀ 𝑣 ( ( 𝑧 𝐹 𝑢 ∧ 𝑧 𝐹 𝑣 ) → 𝑢 = 𝑣 ) ) )
65 1 2 3 fliftrel ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑅 × 𝑆 ) )
66 relxp ⊢ Rel ( 𝑅 × 𝑆 )
67 relss ⊢ ( 𝐹 ⊆ ( 𝑅 × 𝑆 ) → ( Rel ( 𝑅 × 𝑆 ) → Rel 𝐹 ) )
68 65 66 67 mpisyl ⊢ ( 𝜑 → Rel 𝐹 )
69 dffun2 ⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑧 ∀ 𝑢 ∀ 𝑣 ( ( 𝑧 𝐹 𝑢 ∧ 𝑧 𝐹 𝑣 ) → 𝑢 = 𝑣 ) ) )
70 69 baib ⊢ ( Rel 𝐹 → ( Fun 𝐹 ↔ ∀ 𝑧 ∀ 𝑢 ∀ 𝑣 ( ( 𝑧 𝐹 𝑢 ∧ 𝑧 𝐹 𝑣 ) → 𝑢 = 𝑣 ) ) )
71 68 70 syl ⊢ ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑧 ∀ 𝑢 ∀ 𝑣 ( ( 𝑧 𝐹 𝑢 ∧ 𝑧 𝐹 𝑣 ) → 𝑢 = 𝑣 ) ) )
72 64 71 sylibrd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) → Fun 𝐹 ) )
73 35 72 impbid ⊢ ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) ) )