Theorem constr1trl 23640

Description: Construction of a trail from one given edge in a graph. (Contributed by Alexander van der Vekens, 3-Dec-2017.)

Hypotheses

Ref	Expression
1trl.f	|- F = { <. 0 , i >. }
1trl.p	|- P = { <. 0 , A >. , <. 1 , B >. }

Assertion

Ref	Expression
constr1trl	|- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> F ( V Trails E ) P )

Proof of Theorem constr1trl

Dummy variable k is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1trl.f	. . 3 |- F = { <. 0 , i >. }
2		c0ex 9492	. . . . . . 7 |- 0 e. _V
3		vex 3081	. . . . . . 7 |- i e. _V
4	2, 3	f1osn 5787	. . . . . 6 |- { <. 0 , i >. } : { 0 } -1-1-onto-> { i }
5		f1of1 5749	. . . . . 6 |- ( { <. 0 , i >. } : { 0 } -1-1-onto-> { i } -> { <. 0 , i >. } : { 0 } -1-1-> { i } )
6		fveq2 5800	. . . . . . . . . . . . . . . 16 |- ( F = { <. 0 , i >. } -> ( # ` F ) = ( # ` { <. 0 , i >. } ) )
7		opex 4665	. . . . . . . . . . . . . . . . 17 |- <. 0 , i >. e. _V
8		hashsng 12254	. . . . . . . . . . . . . . . . 17 |- ( <. 0 , i >. e. _V -> ( # ` { <. 0 , i >. } ) = 1 )
9	7, 8	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( # ` { <. 0 , i >. } ) = 1
10	6, 9	syl6eq 2511	. . . . . . . . . . . . . . 15 |- ( F = { <. 0 , i >. } -> ( # ` F ) = 1 )
11	1, 10	ax-mp 5	. . . . . . . . . . . . . 14 |- ( # ` F ) = 1
12	11	oveq2i 6212	. . . . . . . . . . . . 13 |- ( 0..^ ( # ` F ) ) = ( 0..^ 1 )
13		fzo01 11730	. . . . . . . . . . . . 13 |- ( 0..^ 1 ) = { 0 }
14	12, 13	eqtri 2483	. . . . . . . . . . . 12 |- ( 0..^ ( # ` F ) ) = { 0 }
15	14	eqcomi 2467	. . . . . . . . . . 11 |- { 0 } = ( 0..^ ( # ` F ) )
16		f1eq2 5711	. . . . . . . . . . 11 |- ( { 0 } = ( 0..^ ( # ` F ) ) -> ( { <. 0 , i >. } : { 0 } -1-1-> { i } <-> { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> { i } ) )
17	15, 16	ax-mp 5	. . . . . . . . . 10 |- ( { <. 0 , i >. } : { 0 } -1-1-> { i } <-> { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> { i } )
18	17	biimpi 194	. . . . . . . . 9 |- ( { <. 0 , i >. } : { 0 } -1-1-> { i } -> { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> { i } )
19	18	adantr 465	. . . . . . . 8 |- ( ( { <. 0 , i >. } : { 0 } -1-1-> { i } /\ ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) ) -> { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> { i } )
20		prid1g 4090	. . . . . . . . . . . . . 14 |- ( A e. V -> A e. { A , B } )
21	20	adantr 465	. . . . . . . . . . . . 13 |- ( ( A e. V /\ B e. V ) -> A e. { A , B } )
22	21	3ad2ant2 1010	. . . . . . . . . . . 12 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> A e. { A , B } )
23	22	adantl 466	. . . . . . . . . . 11 |- ( ( { <. 0 , i >. } : { 0 } -1-1-> { i } /\ ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) ) -> A e. { A , B } )
24		eleq2 2527	. . . . . . . . . . . . 13 |- ( ( E ` i ) = { A , B } -> ( A e. ( E ` i ) <-> A e. { A , B } ) )
25	24	3ad2ant3 1011	. . . . . . . . . . . 12 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( A e. ( E ` i ) <-> A e. { A , B } ) )
26	25	adantl 466	. . . . . . . . . . 11 |- ( ( { <. 0 , i >. } : { 0 } -1-1-> { i } /\ ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) ) -> ( A e. ( E ` i ) <-> A e. { A , B } ) )
27	23, 26	mpbird 232	. . . . . . . . . 10 |- ( ( { <. 0 , i >. } : { 0 } -1-1-> { i } /\ ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) ) -> A e. ( E ` i ) )
28		elfvdm 5826	. . . . . . . . . 10 |- ( A e. ( E ` i ) -> i e. dom E )
29	27, 28	syl 16	. . . . . . . . 9 |- ( ( { <. 0 , i >. } : { 0 } -1-1-> { i } /\ ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) ) -> i e. dom E )
30	29	snssd 4127	. . . . . . . 8 |- ( ( { <. 0 , i >. } : { 0 } -1-1-> { i } /\ ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) ) -> { i } C_ dom E )
31		f1ss 5720	. . . . . . . 8 |- ( ( { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> { i } /\ { i } C_ dom E ) -> { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> dom E )
32	19, 30, 31	syl2anc 661	. . . . . . 7 |- ( ( { <. 0 , i >. } : { 0 } -1-1-> { i } /\ ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) ) -> { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> dom E )
33	32	ex 434	. . . . . 6 |- ( { <. 0 , i >. } : { 0 } -1-1-> { i } -> ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> dom E ) )
34	4, 5, 33	mp2b 10	. . . . 5 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> dom E )
35	34	adantl 466	. . . 4 |- ( ( F = { <. 0 , i >. } /\ ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) ) -> { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> dom E )
36		f1eq1 5710	. . . . 5 |- ( F = { <. 0 , i >. } -> ( F : ( 0..^ ( # ` F ) ) -1-1-> dom E <-> { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> dom E ) )
37	36	adantr 465	. . . 4 |- ( ( F = { <. 0 , i >. } /\ ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) ) -> ( F : ( 0..^ ( # ` F ) ) -1-1-> dom E <-> { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> dom E ) )
38	35, 37	mpbird 232	. . 3 |- ( ( F = { <. 0 , i >. } /\ ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) ) -> F : ( 0..^ ( # ` F ) ) -1-1-> dom E )
39	1, 38	mpan 670	. 2 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> F : ( 0..^ ( # ` F ) ) -1-1-> dom E )
40		1trl.p	. . . 4 |- P = { <. 0 , A >. , <. 1 , B >. }
41		0z 10769	. . . . . . . . 9 |- 0 e. ZZ
42		1z 10788	. . . . . . . . 9 |- 1 e. ZZ
43	41, 42	pm3.2i 455	. . . . . . . 8 |- ( 0 e. ZZ /\ 1 e. ZZ )
44		0ne1 10501	. . . . . . . 8 |- 0 =/= 1
45		fprg 6001	. . . . . . . . 9 |- ( ( ( 0 e. ZZ /\ 1 e. ZZ ) /\ ( A e. V /\ B e. V ) /\ 0 =/= 1 ) -> { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } --> { A , B } )
46		0p1e1 10545	. . . . . . . . . . . . 13 |- ( 0 + 1 ) = 1
47	46	eqcomi 2467	. . . . . . . . . . . 12 |- 1 = ( 0 + 1 )
48	47	oveq2i 6212	. . . . . . . . . . 11 |- ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
49		fzpr 11629	. . . . . . . . . . . 12 |- ( 0 e. ZZ -> ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
50	41, 49	ax-mp 5	. . . . . . . . . . 11 |- ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) }
51	46	preq2i 4067	. . . . . . . . . . 11 |- { 0 , ( 0 + 1 ) } = { 0 , 1 }
52	48, 50, 51	3eqtri 2487	. . . . . . . . . 10 |- ( 0 ... 1 ) = { 0 , 1 }
53	52	feq2i 5661	. . . . . . . . 9 |- ( { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> { A , B } <-> { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } --> { A , B } )
54	45, 53	sylibr 212	. . . . . . . 8 |- ( ( ( 0 e. ZZ /\ 1 e. ZZ ) /\ ( A e. V /\ B e. V ) /\ 0 =/= 1 ) -> { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> { A , B } )
55	43, 44, 54	mp3an13 1306	. . . . . . 7 |- ( ( A e. V /\ B e. V ) -> { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> { A , B } )
56		prssi 4138	. . . . . . 7 |- ( ( A e. V /\ B e. V ) -> { A , B } C_ V )
57		fss 5676	. . . . . . 7 |- ( ( { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> { A , B } /\ { A , B } C_ V ) -> { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> V )
58	55, 56, 57	syl2anc 661	. . . . . 6 |- ( ( A e. V /\ B e. V ) -> { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> V )
59	58	adantl 466	. . . . 5 |- ( ( P = { <. 0 , A >. , <. 1 , B >. } /\ ( A e. V /\ B e. V ) ) -> { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> V )
60		id 22	. . . . . . 7 |- ( P = { <. 0 , A >. , <. 1 , B >. } -> P = { <. 0 , A >. , <. 1 , B >. } )
61	11	oveq2i 6212	. . . . . . . 8 |- ( 0 ... ( # ` F ) ) = ( 0 ... 1 )
62	61	a1i 11	. . . . . . 7 |- ( P = { <. 0 , A >. , <. 1 , B >. } -> ( 0 ... ( # ` F ) ) = ( 0 ... 1 ) )
63	60, 62	feq12d 5657	. . . . . 6 |- ( P = { <. 0 , A >. , <. 1 , B >. } -> ( P : ( 0 ... ( # ` F ) ) --> V <-> { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> V ) )
64	63	adantr 465	. . . . 5 |- ( ( P = { <. 0 , A >. , <. 1 , B >. } /\ ( A e. V /\ B e. V ) ) -> ( P : ( 0 ... ( # ` F ) ) --> V <-> { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> V ) )
65	59, 64	mpbird 232	. . . 4 |- ( ( P = { <. 0 , A >. , <. 1 , B >. } /\ ( A e. V /\ B e. V ) ) -> P : ( 0 ... ( # ` F ) ) --> V )
66	40, 65	mpan 670	. . 3 |- ( ( A e. V /\ B e. V ) -> P : ( 0 ... ( # ` F ) ) --> V )
67	66	3ad2ant2 1010	. 2 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> P : ( 0 ... ( # ` F ) ) --> V )
68		id 22	. . . . . 6 |- ( ( E ` i ) = { A , B } -> ( E ` i ) = { A , B } )
69	68	3ad2ant3 1011	. . . . 5 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( E ` i ) = { A , B } )
70		fveq1 5799	. . . . . . . . 9 |- ( F = { <. 0 , i >. } -> ( F ` 0 ) = ( { <. 0 , i >. } ` 0 ) )
71	2, 3	fvsn 6021	. . . . . . . . 9 |- ( { <. 0 , i >. } ` 0 ) = i
72	70, 71	syl6eq 2511	. . . . . . . 8 |- ( F = { <. 0 , i >. } -> ( F ` 0 ) = i )
73	1, 72	ax-mp 5	. . . . . . 7 |- ( F ` 0 ) = i
74	73	a1i 11	. . . . . 6 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( F ` 0 ) = i )
75	74	fveq2d 5804	. . . . 5 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( E ` ( F ` 0 ) ) = ( E ` i ) )
76		fveq1 5799	. . . . . . . . . 10 |- ( P = { <. 0 , A >. , <. 1 , B >. } -> ( P ` 0 ) = ( { <. 0 , A >. , <. 1 , B >. } ` 0 ) )
77		fvpr1g 6033	. . . . . . . . . . 11 |- ( ( 0 e. _V /\ A e. V /\ 0 =/= 1 ) -> ( { <. 0 , A >. , <. 1 , B >. } ` 0 ) = A )
78	2, 44, 77	mp3an13 1306	. . . . . . . . . 10 |- ( A e. V -> ( { <. 0 , A >. , <. 1 , B >. } ` 0 ) = A )
79	76, 78	sylan9eq 2515	. . . . . . . . 9 |- ( ( P = { <. 0 , A >. , <. 1 , B >. } /\ A e. V ) -> ( P ` 0 ) = A )
80	40, 79	mpan 670	. . . . . . . 8 |- ( A e. V -> ( P ` 0 ) = A )
81	80	adantr 465	. . . . . . 7 |- ( ( A e. V /\ B e. V ) -> ( P ` 0 ) = A )
82	81	3ad2ant2 1010	. . . . . 6 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( P ` 0 ) = A )
83		fveq1 5799	. . . . . . . . . 10 |- ( P = { <. 0 , A >. , <. 1 , B >. } -> ( P ` 1 ) = ( { <. 0 , A >. , <. 1 , B >. } ` 1 ) )
84		1ex 9493	. . . . . . . . . . 11 |- 1 e. _V
85		fvpr2g 6034	. . . . . . . . . . 11 |- ( ( 1 e. _V /\ B e. V /\ 0 =/= 1 ) -> ( { <. 0 , A >. , <. 1 , B >. } ` 1 ) = B )
86	84, 44, 85	mp3an13 1306	. . . . . . . . . 10 |- ( B e. V -> ( { <. 0 , A >. , <. 1 , B >. } ` 1 ) = B )
87	83, 86	sylan9eq 2515	. . . . . . . . 9 |- ( ( P = { <. 0 , A >. , <. 1 , B >. } /\ B e. V ) -> ( P ` 1 ) = B )
88	40, 87	mpan 670	. . . . . . . 8 |- ( B e. V -> ( P ` 1 ) = B )
89	88	adantl 466	. . . . . . 7 |- ( ( A e. V /\ B e. V ) -> ( P ` 1 ) = B )
90	89	3ad2ant2 1010	. . . . . 6 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( P ` 1 ) = B )
91	82, 90	preq12d 4071	. . . . 5 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> { ( P ` 0 ) , ( P ` 1 ) } = { A , B } )
92	69, 75, 91	3eqtr4d 2505	. . . 4 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( E ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } )
93		fveq2 5800	. . . . . . 7 |- ( k = 0 -> ( F ` k ) = ( F ` 0 ) )
94	93	fveq2d 5804	. . . . . 6 |- ( k = 0 -> ( E ` ( F ` k ) ) = ( E ` ( F ` 0 ) ) )
95		fveq2 5800	. . . . . . 7 |- ( k = 0 -> ( P ` k ) = ( P ` 0 ) )
96		oveq1 6208	. . . . . . . . 9 |- ( k = 0 -> ( k + 1 ) = ( 0 + 1 ) )
97	96, 46	syl6eq 2511	. . . . . . . 8 |- ( k = 0 -> ( k + 1 ) = 1 )
98	97	fveq2d 5804	. . . . . . 7 |- ( k = 0 -> ( P ` ( k + 1 ) ) = ( P ` 1 ) )
99	95, 98	preq12d 4071	. . . . . 6 |- ( k = 0 -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` 0 ) , ( P ` 1 ) } )
100	94, 99	eqeq12d 2476	. . . . 5 |- ( k = 0 -> ( ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( E ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } ) )
101	2, 100	ralsn 4024	. . . 4 |- ( A. k e. { 0 } ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( E ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } )
102	92, 101	sylibr 212	. . 3 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> A. k e. { 0 } ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
103	14	a1i 11	. . . 4 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( 0..^ ( # ` F ) ) = { 0 } )
104	103	raleqdv 3029	. . 3 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( A. k e. ( 0..^ ( # ` F ) ) ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> A. k e. { 0 } ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
105	102, 104	mpbird 232	. 2 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> A. k e. ( 0..^ ( # ` F ) ) ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
106		snex 4642	. . . . 5 |- { <. 0 , i >. } e. _V
107	1, 106	eqeltri 2538	. . . 4 |- F e. _V
108		prex 4643	. . . . 5 |- { <. 0 , A >. , <. 1 , B >. } e. _V
109	40, 108	eqeltri 2538	. . . 4 |- P e. _V
110		istrl2 23590	. . . 4 |- ( ( ( V e. X /\ E e. Y ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( V Trails E ) P <-> ( F : ( 0..^ ( # ` F ) ) -1-1-> dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0..^ ( # ` F ) ) ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
111	107, 109, 110	mpanr12 685	. . 3 |- ( ( V e. X /\ E e. Y ) -> ( F ( V Trails E ) P <-> ( F : ( 0..^ ( # ` F ) ) -1-1-> dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0..^ ( # ` F ) ) ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
112	111	3ad2ant1 1009	. 2 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( F ( V Trails E ) P <-> ( F : ( 0..^ ( # ` F ) ) -1-1-> dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0..^ ( # ` F ) ) ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
113	39, 67, 105, 112	mpbir3and 1171	1 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> F ( V Trails E ) P )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1758   =/= wne 2648   A.wral 2799   _Vcvv 3078   C_ wss 3437   {csn 3986   {cpr 3988   <.cop 3992   class class class wbr 4401   dom cdm 4949   -->wf 5523   -1-1->wf1 5524   -1-1-onto->wf1o 5526   ` cfv 5527  (class class class)co 6201   0cc0 9394   1c1 9395   + caddc 9397   ZZcz 10758   ...cfz 11555  ..^cfzo 11666   #chash 12221   Trails ctrail 23559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4512  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483  ax-cnex 9450  ax-resscn 9451  ax-1cn 9452  ax-icn 9453  ax-addcl 9454  ax-addrcl 9455  ax-mulcl 9456  ax-mulrcl 9457  ax-mulcom 9458  ax-addass 9459  ax-mulass 9460  ax-distr 9461  ax-i2m1 9462  ax-1ne0 9463  ax-1rid 9464  ax-rnegex 9465  ax-rrecex 9466  ax-cnre 9467  ax-pre-lttri 9468  ax-pre-lttrn 9469  ax-pre-ltadd 9470  ax-pre-mulgt0 9471

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-tp 3991  df-op 3993  df-uni 4201  df-int 4238  df-iun 4282  df-br 4402  df-opab 4460  df-mpt 4461  df-tr 4495  df-eprel 4741  df-id 4745  df-po 4750  df-so 4751  df-fr 4788  df-we 4790  df-ord 4831  df-on 4832  df-lim 4833  df-suc 4834  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-riota 6162  df-ov 6204  df-oprab 6205  df-mpt2 6206  df-om 6588  df-1st 6688  df-2nd 6689  df-recs 6943  df-rdg 6977  df-1o 7031  df-oadd 7035  df-er 7212  df-map 7327  df-pm 7328  df-en 7422  df-dom 7423  df-sdom 7424  df-fin 7425  df-card 8221  df-pnf 9532  df-mnf 9533  df-xr 9534  df-ltxr 9535  df-le 9536  df-sub 9709  df-neg 9710  df-nn 10435  df-n0 10692  df-z 10759  df-uz 10974  df-fz 11556  df-fzo 11667  df-hash 12222  df-word 12348  df-wlk 23568  df-trail 23569

This theorem is referenced by:  1pthon  23643