Theorem constr1trl 25311

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 9634	. . . . . . 7 |- 0 e. _V
3		vex 3047	. . . . . . 7 |- i e. _V
4	2, 3	f1osn 5850	. . . . . 6 |- { <. 0 , i >. } : { 0 } -1-1-onto-> { i }
5		f1of1 5811	. . . . . 6 |- ( { <. 0 , i >. } : { 0 } -1-1-onto-> { i } -> { <. 0 , i >. } : { 0 } -1-1-> { i } )
6		fveq2 5863	. . . . . . . . . . . . . . . 16 |- ( F = { <. 0 , i >. } -> ( # ` F ) = ( # ` { <. 0 , i >. } ) )
7		opex 4663	. . . . . . . . . . . . . . . . 17 |- <. 0 , i >. e. _V
8		hashsng 12546	. . . . . . . . . . . . . . . . 17 |- ( <. 0 , i >. e. _V -> ( # ` { <. 0 , i >. } ) = 1 )
9	7, 8	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( # ` { <. 0 , i >. } ) = 1
10	6, 9	syl6eq 2500	. . . . . . . . . . . . . . 15 |- ( F = { <. 0 , i >. } -> ( # ` F ) = 1 )
11	1, 10	ax-mp 5	. . . . . . . . . . . . . 14 |- ( # ` F ) = 1
12	11	oveq2i 6299	. . . . . . . . . . . . 13 |- ( 0..^ ( # ` F ) ) = ( 0..^ 1 )
13		fzo01 11992	. . . . . . . . . . . . 13 |- ( 0..^ 1 ) = { 0 }
14	12, 13	eqtri 2472	. . . . . . . . . . . 12 |- ( 0..^ ( # ` F ) ) = { 0 }
15	14	eqcomi 2459	. . . . . . . . . . 11 |- { 0 } = ( 0..^ ( # ` F ) )
16		f1eq2 5773	. . . . . . . . . . 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 198	. . . . . . . . 9 |- ( { <. 0 , i >. } : { 0 } -1-1-> { i } -> { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> { i } )
19	18	adantr 467	. . . . . . . 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 4077	. . . . . . . . . . . . . 14 |- ( A e. V -> A e. { A , B } )
21	20	adantr 467	. . . . . . . . . . . . 13 |- ( ( A e. V /\ B e. V ) -> A e. { A , B } )
22	21	3ad2ant2 1029	. . . . . . . . . . . 12 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> A e. { A , B } )
23	22	adantl 468	. . . . . . . . . . 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 2517	. . . . . . . . . . . . 13 |- ( ( E ` i ) = { A , B } -> ( A e. ( E ` i ) <-> A e. { A , B } ) )
25	24	3ad2ant3 1030	. . . . . . . . . . . 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 468	. . . . . . . . . . 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 236	. . . . . . . . . 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 5889	. . . . . . . . . 10 |- ( A e. ( E ` i ) -> i e. dom E )
29	27, 28	syl 17	. . . . . . . . 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 4116	. . . . . . . 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 5782	. . . . . . . 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 666	. . . . . . 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 436	. . . . . 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 468	. . . 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 5772	. . . . 5 |- ( F = { <. 0 , i >. } -> ( F : ( 0..^ ( # ` F ) ) -1-1-> dom E <-> { <. 0 , i >. } : ( 0..^ ( # ` F ) ) -1-1-> dom E ) )
37	36	adantr 467	. . . 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 236	. . 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 675	. 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 10945	. . . . . . . . 9 |- 0 e. ZZ
42		1z 10964	. . . . . . . . 9 |- 1 e. ZZ
43	41, 42	pm3.2i 457	. . . . . . . 8 |- ( 0 e. ZZ /\ 1 e. ZZ )
44		0ne1 10674	. . . . . . . 8 |- 0 =/= 1
45		fprg 6071	. . . . . . . . 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 10718	. . . . . . . . . . . . 13 |- ( 0 + 1 ) = 1
47	46	eqcomi 2459	. . . . . . . . . . . 12 |- 1 = ( 0 + 1 )
48	47	oveq2i 6299	. . . . . . . . . . 11 |- ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
49		fzpr 11848	. . . . . . . . . . . 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 4054	. . . . . . . . . . 11 |- { 0 , ( 0 + 1 ) } = { 0 , 1 }
52	48, 50, 51	3eqtri 2476	. . . . . . . . . 10 |- ( 0 ... 1 ) = { 0 , 1 }
53	52	feq2i 5719	. . . . . . . . 9 |- ( { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> { A , B } <-> { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } --> { A , B } )
54	45, 53	sylibr 216	. . . . . . . 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 1354	. . . . . . 7 |- ( ( A e. V /\ B e. V ) -> { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> { A , B } )
56		prssi 4127	. . . . . . 7 |- ( ( A e. V /\ B e. V ) -> { A , B } C_ V )
57	55, 56	fssd 5736	. . . . . 6 |- ( ( A e. V /\ B e. V ) -> { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> V )
58	57	adantl 468	. . . . 5 |- ( ( P = { <. 0 , A >. , <. 1 , B >. } /\ ( A e. V /\ B e. V ) ) -> { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> V )
59		id 22	. . . . . . 7 |- ( P = { <. 0 , A >. , <. 1 , B >. } -> P = { <. 0 , A >. , <. 1 , B >. } )
60	11	oveq2i 6299	. . . . . . . 8 |- ( 0 ... ( # ` F ) ) = ( 0 ... 1 )
61	60	a1i 11	. . . . . . 7 |- ( P = { <. 0 , A >. , <. 1 , B >. } -> ( 0 ... ( # ` F ) ) = ( 0 ... 1 ) )
62	59, 61	feq12d 5715	. . . . . 6 |- ( P = { <. 0 , A >. , <. 1 , B >. } -> ( P : ( 0 ... ( # ` F ) ) --> V <-> { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> V ) )
63	62	adantr 467	. . . . 5 |- ( ( P = { <. 0 , A >. , <. 1 , B >. } /\ ( A e. V /\ B e. V ) ) -> ( P : ( 0 ... ( # ` F ) ) --> V <-> { <. 0 , A >. , <. 1 , B >. } : ( 0 ... 1 ) --> V ) )
64	58, 63	mpbird 236	. . . 4 |- ( ( P = { <. 0 , A >. , <. 1 , B >. } /\ ( A e. V /\ B e. V ) ) -> P : ( 0 ... ( # ` F ) ) --> V )
65	40, 64	mpan 675	. . 3 |- ( ( A e. V /\ B e. V ) -> P : ( 0 ... ( # ` F ) ) --> V )
66	65	3ad2ant2 1029	. 2 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> P : ( 0 ... ( # ` F ) ) --> V )
67		id 22	. . . . . 6 |- ( ( E ` i ) = { A , B } -> ( E ` i ) = { A , B } )
68	67	3ad2ant3 1030	. . . . 5 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( E ` i ) = { A , B } )
69		fveq1 5862	. . . . . . . . 9 |- ( F = { <. 0 , i >. } -> ( F ` 0 ) = ( { <. 0 , i >. } ` 0 ) )
70	2, 3	fvsn 6095	. . . . . . . . 9 |- ( { <. 0 , i >. } ` 0 ) = i
71	69, 70	syl6eq 2500	. . . . . . . 8 |- ( F = { <. 0 , i >. } -> ( F ` 0 ) = i )
72	1, 71	ax-mp 5	. . . . . . 7 |- ( F ` 0 ) = i
73	72	a1i 11	. . . . . 6 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( F ` 0 ) = i )
74	73	fveq2d 5867	. . . . 5 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( E ` ( F ` 0 ) ) = ( E ` i ) )
75		fveq1 5862	. . . . . . . . . 10 |- ( P = { <. 0 , A >. , <. 1 , B >. } -> ( P ` 0 ) = ( { <. 0 , A >. , <. 1 , B >. } ` 0 ) )
76		fvpr1g 6107	. . . . . . . . . . 11 |- ( ( 0 e. _V /\ A e. V /\ 0 =/= 1 ) -> ( { <. 0 , A >. , <. 1 , B >. } ` 0 ) = A )
77	2, 44, 76	mp3an13 1354	. . . . . . . . . 10 |- ( A e. V -> ( { <. 0 , A >. , <. 1 , B >. } ` 0 ) = A )
78	75, 77	sylan9eq 2504	. . . . . . . . 9 |- ( ( P = { <. 0 , A >. , <. 1 , B >. } /\ A e. V ) -> ( P ` 0 ) = A )
79	40, 78	mpan 675	. . . . . . . 8 |- ( A e. V -> ( P ` 0 ) = A )
80	79	adantr 467	. . . . . . 7 |- ( ( A e. V /\ B e. V ) -> ( P ` 0 ) = A )
81	80	3ad2ant2 1029	. . . . . 6 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( P ` 0 ) = A )
82		fveq1 5862	. . . . . . . . . 10 |- ( P = { <. 0 , A >. , <. 1 , B >. } -> ( P ` 1 ) = ( { <. 0 , A >. , <. 1 , B >. } ` 1 ) )
83		1ex 9635	. . . . . . . . . . 11 |- 1 e. _V
84		fvpr2g 6108	. . . . . . . . . . 11 |- ( ( 1 e. _V /\ B e. V /\ 0 =/= 1 ) -> ( { <. 0 , A >. , <. 1 , B >. } ` 1 ) = B )
85	83, 44, 84	mp3an13 1354	. . . . . . . . . 10 |- ( B e. V -> ( { <. 0 , A >. , <. 1 , B >. } ` 1 ) = B )
86	82, 85	sylan9eq 2504	. . . . . . . . 9 |- ( ( P = { <. 0 , A >. , <. 1 , B >. } /\ B e. V ) -> ( P ` 1 ) = B )
87	40, 86	mpan 675	. . . . . . . 8 |- ( B e. V -> ( P ` 1 ) = B )
88	87	adantl 468	. . . . . . 7 |- ( ( A e. V /\ B e. V ) -> ( P ` 1 ) = B )
89	88	3ad2ant2 1029	. . . . . 6 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( P ` 1 ) = B )
90	81, 89	preq12d 4058	. . . . 5 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> { ( P ` 0 ) , ( P ` 1 ) } = { A , B } )
91	68, 74, 90	3eqtr4d 2494	. . . 4 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( E ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } )
92		fveq2 5863	. . . . . . 7 |- ( k = 0 -> ( F ` k ) = ( F ` 0 ) )
93	92	fveq2d 5867	. . . . . 6 |- ( k = 0 -> ( E ` ( F ` k ) ) = ( E ` ( F ` 0 ) ) )
94		fveq2 5863	. . . . . . 7 |- ( k = 0 -> ( P ` k ) = ( P ` 0 ) )
95		oveq1 6295	. . . . . . . . 9 |- ( k = 0 -> ( k + 1 ) = ( 0 + 1 ) )
96	95, 46	syl6eq 2500	. . . . . . . 8 |- ( k = 0 -> ( k + 1 ) = 1 )
97	96	fveq2d 5867	. . . . . . 7 |- ( k = 0 -> ( P ` ( k + 1 ) ) = ( P ` 1 ) )
98	94, 97	preq12d 4058	. . . . . 6 |- ( k = 0 -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` 0 ) , ( P ` 1 ) } )
99	93, 98	eqeq12d 2465	. . . . 5 |- ( k = 0 -> ( ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( E ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } ) )
100	2, 99	ralsn 4009	. . . 4 |- ( A. k e. { 0 } ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( E ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } )
101	91, 100	sylibr 216	. . 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 ) ) } )
102	14	a1i 11	. . . 4 |- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) /\ ( E ` i ) = { A , B } ) -> ( 0..^ ( # ` F ) ) = { 0 } )
103	102	raleqdv 2992	. . 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 ) ) } ) )
104	101, 103	mpbird 236	. 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 ) ) } )
105		snex 4640	. . . . 5 |- { <. 0 , i >. } e. _V
106	1, 105	eqeltri 2524	. . . 4 |- F e. _V
107		prex 4641	. . . . 5 |- { <. 0 , A >. , <. 1 , B >. } e. _V
108	40, 107	eqeltri 2524	. . . 4 |- P e. _V
109		istrl2 25261	. . . 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 ) ) } ) ) )
110	106, 108, 109	mpanr12 690	. . 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 ) ) } ) ) )
111	110	3ad2ant1 1028	. 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 ) ) } ) ) )
112	39, 66, 104, 111	mpbir3and 1190	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 188   /\ wa 371   /\ w3a 984   = wceq 1443   e. wcel 1886   =/= wne 2621   A.wral 2736   _Vcvv 3044   C_ wss 3403   {csn 3967   {cpr 3969   <.cop 3973   class class class wbr 4401   dom cdm 4833   -->wf 5577   -1-1->wf1 5578   -1-1-onto->wf1o 5580   ` cfv 5581  (class class class)co 6288   0cc0 9536   1c1 9537   + caddc 9539   ZZcz 10934   ...cfz 11781  ..^cfzo 11912   #chash 12512   Trails ctrail 25220

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-oadd 7183  df-er 7360  df-map 7471  df-pm 7472  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-card 8370  df-cda 8595  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-nn 10607  df-2 10665  df-n0 10867  df-z 10935  df-uz 11157  df-fz 11782  df-fzo 11913  df-hash 12513  df-word 12661  df-wlk 25229  df-trail 25230

This theorem is referenced by:  1pthon  25314