Theorem ltfintri 4467

Description: Trichotomy law for finite less than. (Contributed by SF, 29-Jan-2015.)

Assertion

Ref	Expression
ltfintri	|- ((M e. Nn /\ N e. Nn /\ M =/= (/)) -> (<<M, N>> e. <fin \/ M = N \/ <<N, M>> e. <fin ))

Proof of Theorem ltfintri

Dummy variables m n k p are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opkeq2 4061	. . . . . . . 8 |- (n = N -> <<M, n>> = <<M, N>>)
2	1	eleq1d 2419	. . . . . . 7 |- (n = N -> (<<M, n>> e. <fin <-> <<M, N>> e. <fin ))
3		eqeq2 2362	. . . . . . 7 |- (n = N -> (M = n <-> M = N))
4		opkeq1 4060	. . . . . . . 8 |- (n = N -> <<n, M>> = <<N, M>>)
5	4	eleq1d 2419	. . . . . . 7 |- (n = N -> (<<n, M>> e. <fin <-> <<N, M>> e. <fin ))
6	2, 3, 5	3orbi123d 1251	. . . . . 6 |- (n = N -> ((<<M, n>> e. <fin \/ M = n \/ <<n, M>> e. <fin ) <-> (<<M, N>> e. <fin \/ M = N \/ <<N, M>> e. <fin )))
7	6	imbi2d 307	. . . . 5 |- (n = N -> ((M =/= (/) -> (<<M, n>> e. <fin \/ M = n \/ <<n, M>> e. <fin )) <-> (M =/= (/) -> (<<M, N>> e. <fin \/ M = N \/ <<N, M>> e. <fin ))))
8	7	imbi2d 307	. . . 4 |- (n = N -> ((M e. Nn -> (M =/= (/) -> (<<M, n>> e. <fin \/ M = n \/ <<n, M>> e. <fin ))) <-> (M e. Nn -> (M =/= (/) -> (<<M, N>> e. <fin \/ M = N \/ <<N, M>> e. <fin )))))
9		ltfintrilem1 4466	. . . . . 6 |- {k | (n e. Nn -> (k =/= (/) -> (<<k, n>> e. <fin \/ k = n \/ <<n, k>> e. <fin )))} e. _V
10		neeq1 2525	. . . . . . . 8 |- (k = 0c -> (k =/= (/) <-> 0c =/= (/)))
11		opkeq1 4060	. . . . . . . . . 10 |- (k = 0c -> <<k, n>> = <<0c, n>>)
12	11	eleq1d 2419	. . . . . . . . 9 |- (k = 0c -> (<<k, n>> e. <fin <-> <<0c, n>> e. <fin ))
13		eqeq1 2359	. . . . . . . . 9 |- (k = 0c -> (k = n <-> 0c = n))
14		opkeq2 4061	. . . . . . . . . 10 |- (k = 0c -> <<n, k>> = <<n, 0c>>)
15	14	eleq1d 2419	. . . . . . . . 9 |- (k = 0c -> (<<n, k>> e. <fin <-> <<n, 0c>> e. <fin ))
16	12, 13, 15	3orbi123d 1251	. . . . . . . 8 |- (k = 0c -> ((<<k, n>> e. <fin \/ k = n \/ <<n, k>> e. <fin ) <-> (<<0c, n>> e. <fin \/ 0c = n \/ <<n, 0c>> e. <fin )))
17	10, 16	imbi12d 311	. . . . . . 7 |- (k = 0c -> ((k =/= (/) -> (<<k, n>> e. <fin \/ k = n \/ <<n, k>> e. <fin )) <-> (0c =/= (/) -> (<<0c, n>> e. <fin \/ 0c = n \/ <<n, 0c>> e. <fin ))))
18	17	imbi2d 307	. . . . . 6 |- (k = 0c -> ((n e. Nn -> (k =/= (/) -> (<<k, n>> e. <fin \/ k = n \/ <<n, k>> e. <fin ))) <-> (n e. Nn -> (0c =/= (/) -> (<<0c, n>> e. <fin \/ 0c = n \/ <<n, 0c>> e. <fin )))))
19		neeq1 2525	. . . . . . . 8 |- (k = m -> (k =/= (/) <-> m =/= (/)))
20		opkeq1 4060	. . . . . . . . . 10 |- (k = m -> <<k, n>> = <<m, n>>)
21	20	eleq1d 2419	. . . . . . . . 9 |- (k = m -> (<<k, n>> e. <fin <-> <<m, n>> e. <fin ))
22		eqeq1 2359	. . . . . . . . 9 |- (k = m -> (k = n <-> m = n))
23		opkeq2 4061	. . . . . . . . . 10 |- (k = m -> <<n, k>> = <<n, m>>)
24	23	eleq1d 2419	. . . . . . . . 9 |- (k = m -> (<<n, k>> e. <fin <-> <<n, m>> e. <fin ))
25	21, 22, 24	3orbi123d 1251	. . . . . . . 8 |- (k = m -> ((<<k, n>> e. <fin \/ k = n \/ <<n, k>> e. <fin ) <-> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )))
26	19, 25	imbi12d 311	. . . . . . 7 |- (k = m -> ((k =/= (/) -> (<<k, n>> e. <fin \/ k = n \/ <<n, k>> e. <fin )) <-> (m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ))))
27	26	imbi2d 307	. . . . . 6 |- (k = m -> ((n e. Nn -> (k =/= (/) -> (<<k, n>> e. <fin \/ k = n \/ <<n, k>> e. <fin ))) <-> (n e. Nn -> (m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )))))
28		neeq1 2525	. . . . . . . 8 |- (k = (m +o 1c) -> (k =/= (/) <-> (m +o 1c) =/= (/)))
29		opkeq1 4060	. . . . . . . . . 10 |- (k = (m +o 1c) -> <<k, n>> = <<(m +o 1c), n>>)
30	29	eleq1d 2419	. . . . . . . . 9 |- (k = (m +o 1c) -> (<<k, n>> e. <fin <-> <<(m +o 1c), n>> e. <fin ))
31		eqeq1 2359	. . . . . . . . 9 |- (k = (m +o 1c) -> (k = n <-> (m +o 1c) = n))
32		opkeq2 4061	. . . . . . . . . 10 |- (k = (m +o 1c) -> <<n, k>> = <<n, (m +o 1c)>>)
33	32	eleq1d 2419	. . . . . . . . 9 |- (k = (m +o 1c) -> (<<n, k>> e. <fin <-> <<n, (m +o 1c)>> e. <fin ))
34	30, 31, 33	3orbi123d 1251	. . . . . . . 8 |- (k = (m +o 1c) -> ((<<k, n>> e. <fin \/ k = n \/ <<n, k>> e. <fin ) <-> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin )))
35	28, 34	imbi12d 311	. . . . . . 7 |- (k = (m +o 1c) -> ((k =/= (/) -> (<<k, n>> e. <fin \/ k = n \/ <<n, k>> e. <fin )) <-> ((m +o 1c) =/= (/) -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin ))))
36	35	imbi2d 307	. . . . . 6 |- (k = (m +o 1c) -> ((n e. Nn -> (k =/= (/) -> (<<k, n>> e. <fin \/ k = n \/ <<n, k>> e. <fin ))) <-> (n e. Nn -> ((m +o 1c) =/= (/) -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin )))))
37		neeq1 2525	. . . . . . . 8 |- (k = M -> (k =/= (/) <-> M =/= (/)))
38		opkeq1 4060	. . . . . . . . . 10 |- (k = M -> <<k, n>> = <<M, n>>)
39	38	eleq1d 2419	. . . . . . . . 9 |- (k = M -> (<<k, n>> e. <fin <-> <<M, n>> e. <fin ))
40		eqeq1 2359	. . . . . . . . 9 |- (k = M -> (k = n <-> M = n))
41		opkeq2 4061	. . . . . . . . . 10 |- (k = M -> <<n, k>> = <<n, M>>)
42	41	eleq1d 2419	. . . . . . . . 9 |- (k = M -> (<<n, k>> e. <fin <-> <<n, M>> e. <fin ))
43	39, 40, 42	3orbi123d 1251	. . . . . . . 8 |- (k = M -> ((<<k, n>> e. <fin \/ k = n \/ <<n, k>> e. <fin ) <-> (<<M, n>> e. <fin \/ M = n \/ <<n, M>> e. <fin )))
44	37, 43	imbi12d 311	. . . . . . 7 |- (k = M -> ((k =/= (/) -> (<<k, n>> e. <fin \/ k = n \/ <<n, k>> e. <fin )) <-> (M =/= (/) -> (<<M, n>> e. <fin \/ M = n \/ <<n, M>> e. <fin ))))
45	44	imbi2d 307	. . . . . 6 |- (k = M -> ((n e. Nn -> (k =/= (/) -> (<<k, n>> e. <fin \/ k = n \/ <<n, k>> e. <fin ))) <-> (n e. Nn -> (M =/= (/) -> (<<M, n>> e. <fin \/ M = n \/ <<n, M>> e. <fin )))))
46		0cminle 4462	. . . . . . . . . 10 |- (n e. Nn -> <<0c, n>> e. <_fin )
47	46	adantr 451	. . . . . . . . 9 |- ((n e. Nn /\ 0c =/= (/)) -> <<0c, n>> e. <_fin )
48		0cex 4393	. . . . . . . . . . 11 |- 0c e. _V
49		lefinlteq 4464	. . . . . . . . . . 11 |- ((0c e. _V /\ n e. Nn /\ 0c =/= (/)) -> (<<0c, n>> e. <_fin <-> (<<0c, n>> e. <fin \/ 0c = n)))
50	48, 49	mp3an1 1264	. . . . . . . . . 10 |- ((n e. Nn /\ 0c =/= (/)) -> (<<0c, n>> e. <_fin <-> (<<0c, n>> e. <fin \/ 0c = n)))
51		orcom 376	. . . . . . . . . 10 |- ((<<0c, n>> e. <fin \/ 0c = n) <-> (0c = n \/ <<0c, n>> e. <fin ))
52	50, 51	syl6bb 252	. . . . . . . . 9 |- ((n e. Nn /\ 0c =/= (/)) -> (<<0c, n>> e. <_fin <-> (0c = n \/ <<0c, n>> e. <fin )))
53	47, 52	mpbid 201	. . . . . . . 8 |- ((n e. Nn /\ 0c =/= (/)) -> (0c = n \/ <<0c, n>> e. <fin ))
54		3mix2 1125	. . . . . . . . 9 |- (0c = n -> (<<0c, n>> e. <fin \/ 0c = n \/ <<n, 0c>> e. <fin ))
55		3mix1 1124	. . . . . . . . 9 |- (<<0c, n>> e. <fin -> (<<0c, n>> e. <fin \/ 0c = n \/ <<n, 0c>> e. <fin ))
56	54, 55	jaoi 368	. . . . . . . 8 |- ((0c = n \/ <<0c, n>> e. <fin ) -> (<<0c, n>> e. <fin \/ 0c = n \/ <<n, 0c>> e. <fin ))
57	53, 56	syl 15	. . . . . . 7 |- ((n e. Nn /\ 0c =/= (/)) -> (<<0c, n>> e. <fin \/ 0c = n \/ <<n, 0c>> e. <fin ))
58	57	ex 423	. . . . . 6 |- (n e. Nn -> (0c =/= (/) -> (<<0c, n>> e. <fin \/ 0c = n \/ <<n, 0c>> e. <fin )))
59		addcnnul 4454	. . . . . . . . . . . . 13 |- ((m +o 1c) =/= (/) -> (m =/= (/) /\ 1c =/= (/)))
60	59	simpld 445	. . . . . . . . . . . 12 |- ((m +o 1c) =/= (/) -> m =/= (/))
61	60	3ad2ant3 978	. . . . . . . . . . 11 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> m =/= (/))
62		addc32 4417	. . . . . . . . . . . . . . . . . . . 20 |- ((m +o p) +o 1c) = ((m +o 1c) +o p)
63	62	eqeq2i 2363	. . . . . . . . . . . . . . . . . . 19 |- (n = ((m +o p) +o 1c) <-> n = ((m +o 1c) +o p))
64	63	rexbii 2640	. . . . . . . . . . . . . . . . . 18 |- (E.p e. Nn n = ((m +o p) +o 1c) <-> E.p e. Nn n = ((m +o 1c) +o p))
65	64	biimpi 186	. . . . . . . . . . . . . . . . 17 |- (E.p e. Nn n = ((m +o p) +o 1c) -> E.p e. Nn n = ((m +o 1c) +o p))
66	65	adantl 452	. . . . . . . . . . . . . . . 16 |- ((m =/= (/) /\ E.p e. Nn n = ((m +o p) +o 1c)) -> E.p e. Nn n = ((m +o 1c) +o p))
67	66	a1i 10	. . . . . . . . . . . . . . 15 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> ((m =/= (/) /\ E.p e. Nn n = ((m +o p) +o 1c)) -> E.p e. Nn n = ((m +o 1c) +o p)))
68		opkltfing 4450	. . . . . . . . . . . . . . . 16 |- ((m e. Nn /\ n e. Nn ) -> (<<m, n>> e. <fin <-> (m =/= (/) /\ E.p e. Nn n = ((m +o p) +o 1c))))
69	68	3adant3 975	. . . . . . . . . . . . . . 15 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> (<<m, n>> e. <fin <-> (m =/= (/) /\ E.p e. Nn n = ((m +o p) +o 1c))))
70		simp1 955	. . . . . . . . . . . . . . . . 17 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> m e. Nn )
71		peano2 4404	. . . . . . . . . . . . . . . . 17 |- (m e. Nn -> (m +o 1c) e. Nn )
72	70, 71	syl 15	. . . . . . . . . . . . . . . 16 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> (m +o 1c) e. Nn )
73		simp2 956	. . . . . . . . . . . . . . . 16 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> n e. Nn )
74		opklefing 4449	. . . . . . . . . . . . . . . 16 |- (((m +o 1c) e. Nn /\ n e. Nn ) -> (<<(m +o 1c), n>> e. <_fin <-> E.p e. Nn n = ((m +o 1c) +o p)))
75	72, 73, 74	syl2anc 642	. . . . . . . . . . . . . . 15 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> (<<(m +o 1c), n>> e. <_fin <-> E.p e. Nn n = ((m +o 1c) +o p)))
76	67, 69, 75	3imtr4d 259	. . . . . . . . . . . . . 14 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> (<<m, n>> e. <fin -> <<(m +o 1c), n>> e. <_fin ))
77		lefinlteq 4464	. . . . . . . . . . . . . . 15 |- (((m +o 1c) e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> (<<(m +o 1c), n>> e. <_fin <-> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n)))
78	71, 77	syl3an1 1215	. . . . . . . . . . . . . 14 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> (<<(m +o 1c), n>> e. <_fin <-> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n)))
79	76, 78	sylibd 205	. . . . . . . . . . . . 13 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> (<<m, n>> e. <fin -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n)))
80		3mix1 1124	. . . . . . . . . . . . . 14 |- (<<(m +o 1c), n>> e. <fin -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin ))
81		3mix2 1125	. . . . . . . . . . . . . 14 |- ((m +o 1c) = n -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin ))
82	80, 81	jaoi 368	. . . . . . . . . . . . 13 |- ((<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n) -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin ))
83	79, 82	syl6 29	. . . . . . . . . . . 12 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> (<<m, n>> e. <fin -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin )))
84		ltfinp1 4463	. . . . . . . . . . . . . . . 16 |- ((m e. Nn /\ m =/= (/)) -> <<m, (m +o 1c)>> e. <fin )
85	60, 84	sylan2 460	. . . . . . . . . . . . . . 15 |- ((m e. Nn /\ (m +o 1c) =/= (/)) -> <<m, (m +o 1c)>> e. <fin )
86	85	3adant2 974	. . . . . . . . . . . . . 14 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> <<m, (m +o 1c)>> e. <fin )
87		opkeq1 4060	. . . . . . . . . . . . . . 15 |- (m = n -> <<m, (m +o 1c)>> = <<n, (m +o 1c)>>)
88	87	eleq1d 2419	. . . . . . . . . . . . . 14 |- (m = n -> (<<m, (m +o 1c)>> e. <fin <-> <<n, (m +o 1c)>> e. <fin ))
89	86, 88	syl5ibcom 211	. . . . . . . . . . . . 13 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> (m = n -> <<n, (m +o 1c)>> e. <fin ))
90		3mix3 1126	. . . . . . . . . . . . 13 |- (<<n, (m +o 1c)>> e. <fin -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin ))
91	89, 90	syl6 29	. . . . . . . . . . . 12 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> (m = n -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin )))
92		ltfintr 4460	. . . . . . . . . . . . . . 15 |- ((n e. Nn /\ m e. Nn /\ (m +o 1c) e. Nn ) -> ((<<n, m>> e. <fin /\ <<m, (m +o 1c)>> e. <fin ) -> <<n, (m +o 1c)>> e. <fin ))
93	73, 70, 72, 92	syl3anc 1182	. . . . . . . . . . . . . 14 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> ((<<n, m>> e. <fin /\ <<m, (m +o 1c)>> e. <fin ) -> <<n, (m +o 1c)>> e. <fin ))
94	86, 93	mpan2d 655	. . . . . . . . . . . . 13 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> (<<n, m>> e. <fin -> <<n, (m +o 1c)>> e. <fin ))
95	94, 90	syl6 29	. . . . . . . . . . . 12 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> (<<n, m>> e. <fin -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin )))
96	83, 91, 95	3jaod 1246	. . . . . . . . . . 11 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> ((<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ) -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin )))
97	61, 96	embantd 50	. . . . . . . . . 10 |- ((m e. Nn /\ n e. Nn /\ (m +o 1c) =/= (/)) -> ((m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )) -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin )))
98	97	3expia 1153	. . . . . . . . 9 |- ((m e. Nn /\ n e. Nn ) -> ((m +o 1c) =/= (/) -> ((m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )) -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin ))))
99	98	com23 72	. . . . . . . 8 |- ((m e. Nn /\ n e. Nn ) -> ((m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )) -> ((m +o 1c) =/= (/) -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin ))))
100	99	ex 423	. . . . . . 7 |- (m e. Nn -> (n e. Nn -> ((m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )) -> ((m +o 1c) =/= (/) -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin )))))
101	100	a2d 23	. . . . . 6 |- (m e. Nn -> ((n e. Nn -> (m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ))) -> (n e. Nn -> ((m +o 1c) =/= (/) -> (<<(m +o 1c), n>> e. <fin \/ (m +o 1c) = n \/ <<n, (m +o 1c)>> e. <fin )))))
102	9, 18, 27, 36, 45, 58, 101	finds 4412	. . . . 5 |- (M e. Nn -> (n e. Nn -> (M =/= (/) -> (<<M, n>> e. <fin \/ M = n \/ <<n, M>> e. <fin ))))
103	102	com12 27	. . . 4 |- (n e. Nn -> (M e. Nn -> (M =/= (/) -> (<<M, n>> e. <fin \/ M = n \/ <<n, M>> e. <fin ))))
104	8, 103	vtoclga 2921	. . 3 |- (N e. Nn -> (M e. Nn -> (M =/= (/) -> (<<M, N>> e. <fin \/ M = N \/ <<N, M>> e. <fin ))))
105	104	com12 27	. 2 |- (M e. Nn -> (N e. Nn -> (M =/= (/) -> (<<M, N>> e. <fin \/ M = N \/ <<N, M>> e. <fin ))))
106	105	3imp 1145	1 |- ((M e. Nn /\ N e. Nn /\ M =/= (/)) -> (<<M, N>> e. <fin \/ M = N \/ <<N, M>> e. <fin ))

Syntax hints:   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358   \/ w3o 933   /\ w3a 934   = wceq 1642   e. wcel 1710   =/= wne 2517  E.wrex 2616  _Vcvv 2860  (/)c0 3551  <<copk 4058  1_cc1c 4135   Nn cnnc 4374  0_cc0c 4375   +o cplc 4376   <__fin clefin 4433   <_fin cltfin 4434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-0c 4378  df-addc 4379  df-nnc 4380  df-lefin 4441  df-ltfin 4442

This theorem is referenced by:  lenltfin  4470  tfinltfin  4502  sfin111  4537