Metamath Proof Explorer


Theorem elfuns

Description: Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013)

Ref Expression
Hypothesis elfuns.1 F V
Assertion elfuns F 𝖥𝗎𝗇𝗌 Fun F

Proof

Step Hyp Ref Expression
1 elfuns.1 F V
2 elrel Rel F p F x y p = x y
3 2 ex Rel F p F x y p = x y
4 elrel Rel F q F a z q = a z
5 4 ex Rel F q F a z q = a z
6 3 5 anim12d Rel F p F q F x y p = x y a z q = a z
7 6 adantrd Rel F p F q F q 1 st V I 2 nd p x y p = x y a z q = a z
8 7 pm4.71rd Rel F p F q F q 1 st V I 2 nd p x y p = x y a z q = a z p F q F q 1 st V I 2 nd p
9 19.41vvvv x y a z p = x y q = a z p F q F q 1 st V I 2 nd p x y a z p = x y q = a z p F q F q 1 st V I 2 nd p
10 ee4anv x y a z p = x y q = a z x y p = x y a z q = a z
11 10 anbi1i x y a z p = x y q = a z p F q F q 1 st V I 2 nd p x y p = x y a z q = a z p F q F q 1 st V I 2 nd p
12 9 11 bitr2i x y p = x y a z q = a z p F q F q 1 st V I 2 nd p x y a z p = x y q = a z p F q F q 1 st V I 2 nd p
13 8 12 bitrdi Rel F p F q F q 1 st V I 2 nd p x y a z p = x y q = a z p F q F q 1 st V I 2 nd p
14 13 2exbidv Rel F p q p F q F q 1 st V I 2 nd p p q x y a z p = x y q = a z p F q F q 1 st V I 2 nd p
15 excom13 p q x y a z p = x y q = a z p F q F q 1 st V I 2 nd p x q p y a z p = x y q = a z p F q F q 1 st V I 2 nd p
16 excom13 q p y a z p = x y q = a z p F q F q 1 st V I 2 nd p y p q a z p = x y q = a z p F q F q 1 st V I 2 nd p
17 exrot4 p q a z p = x y q = a z p F q F q 1 st V I 2 nd p a z p q p = x y q = a z p F q F q 1 st V I 2 nd p
18 excom a z p q p = x y q = a z p F q F q 1 st V I 2 nd p z a p q p = x y q = a z p F q F q 1 st V I 2 nd p
19 df-3an p = x y q = a z p F q F q 1 st V I 2 nd p p = x y q = a z p F q F q 1 st V I 2 nd p
20 19 2exbii p q p = x y q = a z p F q F q 1 st V I 2 nd p p q p = x y q = a z p F q F q 1 st V I 2 nd p
21 opex x y V
22 opex a z V
23 eleq1 p = x y p F x y F
24 23 anbi1d p = x y p F q F x y F q F
25 breq2 p = x y q 1 st V I 2 nd p q 1 st V I 2 nd x y
26 24 25 anbi12d p = x y p F q F q 1 st V I 2 nd p x y F q F q 1 st V I 2 nd x y
27 eleq1 q = a z q F a z F
28 27 anbi2d q = a z x y F q F x y F a z F
29 breq1 q = a z q 1 st V I 2 nd x y a z 1 st V I 2 nd x y
30 vex x V
31 vex y V
32 22 30 31 brtxp a z 1 st V I 2 nd x y a z 1 st x a z V I 2 nd y
33 vex a V
34 vex z V
35 33 34 br1steq a z 1 st x x = a
36 equcom x = a a = x
37 35 36 bitri a z 1 st x a = x
38 22 31 brco a z V I 2 nd y x a z 2 nd x x V I y
39 33 34 br2ndeq a z 2 nd x x = z
40 39 anbi1i a z 2 nd x x V I y x = z x V I y
41 40 exbii x a z 2 nd x x V I y x x = z x V I y
42 breq1 x = z x V I y z V I y
43 brv z V y
44 brdif z V I y z V y ¬ z I y
45 43 44 mpbiran z V I y ¬ z I y
46 31 ideq z I y z = y
47 equcom z = y y = z
48 46 47 bitri z I y y = z
49 48 notbii ¬ z I y ¬ y = z
50 45 49 bitri z V I y ¬ y = z
51 42 50 bitrdi x = z x V I y ¬ y = z
52 51 equsexvw x x = z x V I y ¬ y = z
53 38 41 52 3bitri a z V I 2 nd y ¬ y = z
54 37 53 anbi12i a z 1 st x a z V I 2 nd y a = x ¬ y = z
55 32 54 bitri a z 1 st V I 2 nd x y a = x ¬ y = z
56 29 55 bitrdi q = a z q 1 st V I 2 nd x y a = x ¬ y = z
57 28 56 anbi12d q = a z x y F q F q 1 st V I 2 nd x y x y F a z F a = x ¬ y = z
58 an12 x y F a z F a = x ¬ y = z a = x x y F a z F ¬ y = z
59 57 58 bitrdi q = a z x y F q F q 1 st V I 2 nd x y a = x x y F a z F ¬ y = z
60 21 22 26 59 ceqsex2v p q p = x y q = a z p F q F q 1 st V I 2 nd p a = x x y F a z F ¬ y = z
61 20 60 bitr3i p q p = x y q = a z p F q F q 1 st V I 2 nd p a = x x y F a z F ¬ y = z
62 61 exbii a p q p = x y q = a z p F q F q 1 st V I 2 nd p a a = x x y F a z F ¬ y = z
63 opeq1 a = x a z = x z
64 63 eleq1d a = x a z F x z F
65 64 anbi2d a = x x y F a z F x y F x z F
66 65 anbi1d a = x x y F a z F ¬ y = z x y F x z F ¬ y = z
67 66 equsexvw a a = x x y F a z F ¬ y = z x y F x z F ¬ y = z
68 62 67 bitri a p q p = x y q = a z p F q F q 1 st V I 2 nd p x y F x z F ¬ y = z
69 68 exbii z a p q p = x y q = a z p F q F q 1 st V I 2 nd p z x y F x z F ¬ y = z
70 exanali z x y F x z F ¬ y = z ¬ z x y F x z F y = z
71 69 70 bitri z a p q p = x y q = a z p F q F q 1 st V I 2 nd p ¬ z x y F x z F y = z
72 17 18 71 3bitri p q a z p = x y q = a z p F q F q 1 st V I 2 nd p ¬ z x y F x z F y = z
73 72 exbii y p q a z p = x y q = a z p F q F q 1 st V I 2 nd p y ¬ z x y F x z F y = z
74 exnal y ¬ z x y F x z F y = z ¬ y z x y F x z F y = z
75 16 73 74 3bitri q p y a z p = x y q = a z p F q F q 1 st V I 2 nd p ¬ y z x y F x z F y = z
76 75 exbii x q p y a z p = x y q = a z p F q F q 1 st V I 2 nd p x ¬ y z x y F x z F y = z
77 exnal x ¬ y z x y F x z F y = z ¬ x y z x y F x z F y = z
78 15 76 77 3bitri p q x y a z p = x y q = a z p F q F q 1 st V I 2 nd p ¬ x y z x y F x z F y = z
79 14 78 bitrdi Rel F p q p F q F q 1 st V I 2 nd p ¬ x y z x y F x z F y = z
80 79 con2bid Rel F x y z x y F x z F y = z ¬ p q p F q F q 1 st V I 2 nd p
81 80 pm5.32i Rel F x y z x y F x z F y = z Rel F ¬ p q p F q F q 1 st V I 2 nd p
82 dffun4 Fun F Rel F x y z x y F x z F y = z
83 df-funs 𝖥𝗎𝗇𝗌 = 𝒫 V × V 𝖥𝗂𝗑 E 1 st V I 2 nd E -1
84 83 eleq2i F 𝖥𝗎𝗇𝗌 F 𝒫 V × V 𝖥𝗂𝗑 E 1 st V I 2 nd E -1
85 eldif F 𝒫 V × V 𝖥𝗂𝗑 E 1 st V I 2 nd E -1 F 𝒫 V × V ¬ F 𝖥𝗂𝗑 E 1 st V I 2 nd E -1
86 1 elpw F 𝒫 V × V F V × V
87 df-rel Rel F F V × V
88 86 87 bitr4i F 𝒫 V × V Rel F
89 1 elfix F 𝖥𝗂𝗑 E 1 st V I 2 nd E -1 F E 1 st V I 2 nd E -1 F
90 1 1 coep F E 1 st V I 2 nd E -1 F p F F 1 st V I 2 nd E -1 p
91 vex p V
92 1 91 coepr F 1 st V I 2 nd E -1 p q F q 1 st V I 2 nd p
93 92 rexbii p F F 1 st V I 2 nd E -1 p p F q F q 1 st V I 2 nd p
94 90 93 bitri F E 1 st V I 2 nd E -1 F p F q F q 1 st V I 2 nd p
95 r2ex p F q F q 1 st V I 2 nd p p q p F q F q 1 st V I 2 nd p
96 89 94 95 3bitri F 𝖥𝗂𝗑 E 1 st V I 2 nd E -1 p q p F q F q 1 st V I 2 nd p
97 96 notbii ¬ F 𝖥𝗂𝗑 E 1 st V I 2 nd E -1 ¬ p q p F q F q 1 st V I 2 nd p
98 88 97 anbi12i F 𝒫 V × V ¬ F 𝖥𝗂𝗑 E 1 st V I 2 nd E -1 Rel F ¬ p q p F q F q 1 st V I 2 nd p
99 84 85 98 3bitri F 𝖥𝗎𝗇𝗌 Rel F ¬ p q p F q F q 1 st V I 2 nd p
100 81 82 99 3bitr4ri F 𝖥𝗎𝗇𝗌 Fun F