Theorem usgrexmplef

Description: Lemma for usgrexmpl . (Contributed by Alexander van der Vekens, 15-Aug-2017)

	Ref	Expression
Hypotheses	usgrexmplef.v	|- V = ( 0 ... 4 )
	usgrexmplef.e	|- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">
Assertion	usgrexmplef	|- E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 }

Proof

Step	Hyp	Ref	Expression
1		usgrexmplef.v	|- V = ( 0 ... 4 )
2		usgrexmplef.e	|- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">
3		usgrexmpldifpr	|- ( ( { 0 , 1 } =/= { 1 , 2 } /\ { 0 , 1 } =/= { 2 , 0 } /\ { 0 , 1 } =/= { 0 , 3 } ) /\ ( { 1 , 2 } =/= { 2 , 0 } /\ { 1 , 2 } =/= { 0 , 3 } /\ { 2 , 0 } =/= { 0 , 3 } ) )
4		prex	|- { 0 , 1 } e. _V
5		prex	|- { 1 , 2 } e. _V
6		prex	|- { 2 , 0 } e. _V
7		prex	|- { 0 , 3 } e. _V
8		s4f1o	|- ( ( ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V ) /\ ( { 2 , 0 } e. _V /\ { 0 , 3 } e. _V ) ) -> ( ( ( { 0 , 1 } =/= { 1 , 2 } /\ { 0 , 1 } =/= { 2 , 0 } /\ { 0 , 1 } =/= { 0 , 3 } ) /\ ( { 1 , 2 } =/= { 2 , 0 } /\ { 1 , 2 } =/= { 0 , 3 } /\ { 2 , 0 } =/= { 0 , 3 } ) ) -> ( E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } "> -> E : dom E -1-1-onto-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) ) ) )
9	4 5 6 7 8	mp4an	|- ( ( ( { 0 , 1 } =/= { 1 , 2 } /\ { 0 , 1 } =/= { 2 , 0 } /\ { 0 , 1 } =/= { 0 , 3 } ) /\ ( { 1 , 2 } =/= { 2 , 0 } /\ { 1 , 2 } =/= { 0 , 3 } /\ { 2 , 0 } =/= { 0 , 3 } ) ) -> ( E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } "> -> E : dom E -1-1-onto-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) ) )
10	3 2 9	mp2	|- E : dom E -1-1-onto-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } )
11		f1of1	|- ( E : dom E -1-1-onto-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) -> E : dom E -1-1-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) )
12		id	|- ( ran E C_ ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) -> ran E C_ ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) )
13		vex	|- p e. _V
14	13	elpr	|- ( p e. { { 0 , 1 } , { 1 , 2 } } <-> ( p = { 0 , 1 } \/ p = { 1 , 2 } ) )
15		0nn0	|- 0 e. NN0
16		4nn0	|- 4 e. NN0
17		0re	|- 0 e. RR
18		4re	|- 4 e. RR
19		4pos	|- 0 < 4
20	17 18 19	ltleii	|- 0 <_ 4
21		elfz2nn0	|- ( 0 e. ( 0 ... 4 ) <-> ( 0 e. NN0 /\ 4 e. NN0 /\ 0 <_ 4 ) )
22	15 16 20 21	mpbir3an	|- 0 e. ( 0 ... 4 )
23	22 1	eleqtrri	|- 0 e. V
24		1nn0	|- 1 e. NN0
25		1re	|- 1 e. RR
26		1lt4	|- 1 < 4
27	25 18 26	ltleii	|- 1 <_ 4
28		elfz2nn0	|- ( 1 e. ( 0 ... 4 ) <-> ( 1 e. NN0 /\ 4 e. NN0 /\ 1 <_ 4 ) )
29	24 16 27 28	mpbir3an	|- 1 e. ( 0 ... 4 )
30	29 1	eleqtrri	|- 1 e. V
31		prelpwi	|- ( ( 0 e. V /\ 1 e. V ) -> { 0 , 1 } e. ~P V )
32		eleq1	|- ( p = { 0 , 1 } -> ( p e. ~P V <-> { 0 , 1 } e. ~P V ) )
33	31 32	syl5ibrcom	|- ( ( 0 e. V /\ 1 e. V ) -> ( p = { 0 , 1 } -> p e. ~P V ) )
34	23 30 33	mp2an	|- ( p = { 0 , 1 } -> p e. ~P V )
35		fveq2	|- ( p = { 0 , 1 } -> ( # ` p ) = ( # ` { 0 , 1 } ) )
36		prhash2ex	|- ( # ` { 0 , 1 } ) = 2
37	35 36	eqtrdi	|- ( p = { 0 , 1 } -> ( # ` p ) = 2 )
38	34 37	jca	|- ( p = { 0 , 1 } -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
39		2nn0	|- 2 e. NN0
40		2re	|- 2 e. RR
41		2lt4	|- 2 < 4
42	40 18 41	ltleii	|- 2 <_ 4
43		elfz2nn0	|- ( 2 e. ( 0 ... 4 ) <-> ( 2 e. NN0 /\ 4 e. NN0 /\ 2 <_ 4 ) )
44	39 16 42 43	mpbir3an	|- 2 e. ( 0 ... 4 )
45	44 1	eleqtrri	|- 2 e. V
46		prelpwi	|- ( ( 1 e. V /\ 2 e. V ) -> { 1 , 2 } e. ~P V )
47		eleq1	|- ( p = { 1 , 2 } -> ( p e. ~P V <-> { 1 , 2 } e. ~P V ) )
48	46 47	syl5ibrcom	|- ( ( 1 e. V /\ 2 e. V ) -> ( p = { 1 , 2 } -> p e. ~P V ) )
49	30 45 48	mp2an	|- ( p = { 1 , 2 } -> p e. ~P V )
50		fveq2	|- ( p = { 1 , 2 } -> ( # ` p ) = ( # ` { 1 , 2 } ) )
51		1ne2	|- 1 =/= 2
52		1nn	|- 1 e. NN
53		2nn	|- 2 e. NN
54		hashprg	|- ( ( 1 e. NN /\ 2 e. NN ) -> ( 1 =/= 2 <-> ( # ` { 1 , 2 } ) = 2 ) )
55	52 53 54	mp2an	|- ( 1 =/= 2 <-> ( # ` { 1 , 2 } ) = 2 )
56	51 55	mpbi	|- ( # ` { 1 , 2 } ) = 2
57	50 56	eqtrdi	|- ( p = { 1 , 2 } -> ( # ` p ) = 2 )
58	49 57	jca	|- ( p = { 1 , 2 } -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
59	38 58	jaoi	|- ( ( p = { 0 , 1 } \/ p = { 1 , 2 } ) -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
60	14 59	sylbi	|- ( p e. { { 0 , 1 } , { 1 , 2 } } -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
61	13	elpr	|- ( p e. { { 2 , 0 } , { 0 , 3 } } <-> ( p = { 2 , 0 } \/ p = { 0 , 3 } ) )
62		prelpwi	|- ( ( 2 e. V /\ 0 e. V ) -> { 2 , 0 } e. ~P V )
63		eleq1	|- ( p = { 2 , 0 } -> ( p e. ~P V <-> { 2 , 0 } e. ~P V ) )
64	62 63	syl5ibrcom	|- ( ( 2 e. V /\ 0 e. V ) -> ( p = { 2 , 0 } -> p e. ~P V ) )
65	45 23 64	mp2an	|- ( p = { 2 , 0 } -> p e. ~P V )
66		fveq2	|- ( p = { 2 , 0 } -> ( # ` p ) = ( # ` { 2 , 0 } ) )
67		2ne0	|- 2 =/= 0
68		2z	|- 2 e. ZZ
69		0z	|- 0 e. ZZ
70		hashprg	|- ( ( 2 e. ZZ /\ 0 e. ZZ ) -> ( 2 =/= 0 <-> ( # ` { 2 , 0 } ) = 2 ) )
71	68 69 70	mp2an	|- ( 2 =/= 0 <-> ( # ` { 2 , 0 } ) = 2 )
72	67 71	mpbi	|- ( # ` { 2 , 0 } ) = 2
73	66 72	eqtrdi	|- ( p = { 2 , 0 } -> ( # ` p ) = 2 )
74	65 73	jca	|- ( p = { 2 , 0 } -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
75		3nn0	|- 3 e. NN0
76		3re	|- 3 e. RR
77		3lt4	|- 3 < 4
78	76 18 77	ltleii	|- 3 <_ 4
79		elfz2nn0	|- ( 3 e. ( 0 ... 4 ) <-> ( 3 e. NN0 /\ 4 e. NN0 /\ 3 <_ 4 ) )
80	75 16 78 79	mpbir3an	|- 3 e. ( 0 ... 4 )
81	80 1	eleqtrri	|- 3 e. V
82		prelpwi	|- ( ( 0 e. V /\ 3 e. V ) -> { 0 , 3 } e. ~P V )
83		eleq1	|- ( p = { 0 , 3 } -> ( p e. ~P V <-> { 0 , 3 } e. ~P V ) )
84	82 83	syl5ibrcom	|- ( ( 0 e. V /\ 3 e. V ) -> ( p = { 0 , 3 } -> p e. ~P V ) )
85	23 81 84	mp2an	|- ( p = { 0 , 3 } -> p e. ~P V )
86		fveq2	|- ( p = { 0 , 3 } -> ( # ` p ) = ( # ` { 0 , 3 } ) )
87		3ne0	|- 3 =/= 0
88	87	necomi	|- 0 =/= 3
89		3z	|- 3 e. ZZ
90		hashprg	|- ( ( 0 e. ZZ /\ 3 e. ZZ ) -> ( 0 =/= 3 <-> ( # ` { 0 , 3 } ) = 2 ) )
91	69 89 90	mp2an	|- ( 0 =/= 3 <-> ( # ` { 0 , 3 } ) = 2 )
92	88 91	mpbi	|- ( # ` { 0 , 3 } ) = 2
93	86 92	eqtrdi	|- ( p = { 0 , 3 } -> ( # ` p ) = 2 )
94	85 93	jca	|- ( p = { 0 , 3 } -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
95	74 94	jaoi	|- ( ( p = { 2 , 0 } \/ p = { 0 , 3 } ) -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
96	61 95	sylbi	|- ( p e. { { 2 , 0 } , { 0 , 3 } } -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
97	60 96	jaoi	|- ( ( p e. { { 0 , 1 } , { 1 , 2 } } \/ p e. { { 2 , 0 } , { 0 , 3 } } ) -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
98		elun	|- ( p e. ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) <-> ( p e. { { 0 , 1 } , { 1 , 2 } } \/ p e. { { 2 , 0 } , { 0 , 3 } } ) )
99		fveqeq2	|- ( e = p -> ( ( # ` e ) = 2 <-> ( # ` p ) = 2 ) )
100	99	elrab	|- ( p e. { e e. ~P V | ( # ` e ) = 2 } <-> ( p e. ~P V /\ ( # ` p ) = 2 ) )
101	97 98 100	3imtr4i	|- ( p e. ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) -> p e. { e e. ~P V | ( # ` e ) = 2 } )
102	101	ssriv	|- ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) C_ { e e. ~P V | ( # ` e ) = 2 }
103	12 102	sstrdi	|- ( ran E C_ ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) -> ran E C_ { e e. ~P V | ( # ` e ) = 2 } )
104	103	anim2i	|- ( ( E Fn dom E /\ ran E C_ ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) ) -> ( E Fn dom E /\ ran E C_ { e e. ~P V | ( # ` e ) = 2 } ) )
105		df-f	|- ( E : dom E --> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) <-> ( E Fn dom E /\ ran E C_ ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) ) )
106		df-f	|- ( E : dom E --> { e e. ~P V | ( # ` e ) = 2 } <-> ( E Fn dom E /\ ran E C_ { e e. ~P V | ( # ` e ) = 2 } ) )
107	104 105 106	3imtr4i	|- ( E : dom E --> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) -> E : dom E --> { e e. ~P V | ( # ` e ) = 2 } )
108	107	anim1i	|- ( ( E : dom E --> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) /\ A. x E* y y E x ) -> ( E : dom E --> { e e. ~P V | ( # ` e ) = 2 } /\ A. x E* y y E x ) )
109		dff12	|- ( E : dom E -1-1-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) <-> ( E : dom E --> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) /\ A. x E* y y E x ) )
110		dff12	|- ( E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } <-> ( E : dom E --> { e e. ~P V | ( # ` e ) = 2 } /\ A. x E* y y E x ) )
111	108 109 110	3imtr4i	|- ( E : dom E -1-1-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) -> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } )
112	10 11 111	mp2b	|- E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 }