sfintfin - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > sfintfin		Unicode version

Theorem sfintfin 4533

Description: If two numbers obey S_fin, then do their T raisings. Theorem X.1.45 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)

**Assertion**
Ref	Expression
sfintfin	S_fin S_fin T_fin T_fin

Proof of Theorem sfintfin Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-sfin 4447	. . 3 S_fin Nn $/\$ Nn $/\$ ₁ $/\$
2		3simpa 952	. . 3 Nn $/\$ Nn $/\$ ₁ $/\$ Nn $/\$ Nn
3	1, 2	sylbi 187	. 2 S_fin Nn $/\$ Nn
4		sfintfinlem1 4532	. . . 4 S_fin S_fin T_fin T_fin
5		sfineq1 4527	. . . . . 6 0_c S_fin S_fin 0_c
6		tfineq 4489	. . . . . . . 8 0_c T_fin T_fin 0_c
7		tfin0c 4498	. . . . . . . 8 T_fin 0_c 0_c
8	6, 7	syl6eq 2401	. . . . . . 7 0_c T_fin 0_c
9		sfineq1 4527	. . . . . . 7 T_fin 0_c S_fin T_fin T_fin S_fin 0_c T_fin
10	8, 9	syl 15	. . . . . 6 0_c S_fin T_fin T_fin S_fin 0_c T_fin
11	5, 10	imbi12d 311	. . . . 5 0_c S_fin S_fin T_fin T_fin S_fin 0_c S_fin 0_c T_fin
12	11	albidv 1625	. . . 4 0_c S_fin S_fin T_fin T_fin S_fin 0_c S_fin 0_c T_fin
13		sfineq1 4527	. . . . . . 7 S_fin S_fin
14		tfineq 4489	. . . . . . . 8 T_fin T_fin
15		sfineq1 4527	. . . . . . . 8 T_fin T_fin S_fin T_fin T_fin S_fin T_fin T_fin
16	14, 15	syl 15	. . . . . . 7 S_fin T_fin T_fin S_fin T_fin T_fin
17	13, 16	imbi12d 311	. . . . . 6 S_fin S_fin T_fin T_fin S_fin S_fin T_fin T_fin
18	17	albidv 1625	. . . . 5 S_fin S_fin T_fin T_fin S_fin S_fin T_fin T_fin
19		sfineq2 4528	. . . . . . 7 S_fin S_fin
20		tfineq 4489	. . . . . . . 8 T_fin T_fin
21		sfineq2 4528	. . . . . . . 8 T_fin T_fin S_fin T_fin T_fin S_fin T_fin T_fin
22	20, 21	syl 15	. . . . . . 7 S_fin T_fin T_fin S_fin T_fin T_fin
23	19, 22	imbi12d 311	. . . . . 6 S_fin S_fin T_fin T_fin S_fin S_fin T_fin T_fin
24	23	cbvalv 2002	. . . . 5 S_fin S_fin T_fin T_fin S_fin S_fin T_fin T_fin
25	18, 24	syl6bb 252	. . . 4 S_fin S_fin T_fin T_fin S_fin S_fin T_fin T_fin
26		sfineq1 4527	. . . . . 6 1_c S_fin S_fin 1_c
27		tfineq 4489	. . . . . . 7 1_c T_fin T_fin 1_c
28		sfineq1 4527	. . . . . . 7 T_fin T_fin 1_c S_fin T_fin T_fin S_fin T_fin 1_c T_fin
29	27, 28	syl 15	. . . . . 6 1_c S_fin T_fin T_fin S_fin T_fin 1_c T_fin
30	26, 29	imbi12d 311	. . . . 5 1_c S_fin S_fin T_fin T_fin S_fin 1_c S_fin T_fin 1_c T_fin
31	30	albidv 1625	. . . 4 1_c S_fin S_fin T_fin T_fin S_fin 1_c S_fin T_fin 1_c T_fin
32		sfineq1 4527	. . . . . 6 S_fin S_fin
33		tfineq 4489	. . . . . . 7 T_fin T_fin
34		sfineq1 4527	. . . . . . 7 T_fin T_fin S_fin T_fin T_fin S_fin T_fin T_fin
35	33, 34	syl 15	. . . . . 6 S_fin T_fin T_fin S_fin T_fin T_fin
36	32, 35	imbi12d 311	. . . . 5 S_fin S_fin T_fin T_fin S_fin S_fin T_fin T_fin
37	36	albidv 1625	. . . 4 S_fin S_fin T_fin T_fin S_fin S_fin T_fin T_fin
38		sfin01 4529	. . . . . . 7 S_fin 0_c 1_c
39		sfin112 4530	. . . . . . 7 S_fin 0_c $/\$ S_fin 0_c 1_c 1_c
40	38, 39	mpan2 652	. . . . . 6 S_fin 0_c 1_c
41		tfineq 4489	. . . . . . . . 9 1_c T_fin T_fin 1_c
42		tfin1c 4500	. . . . . . . . 9 T_fin 1_c 1_c
43	41, 42	syl6eq 2401	. . . . . . . 8 1_c T_fin 1_c
44		sfineq2 4528	. . . . . . . 8 T_fin 1_c S_fin 0_c T_fin S_fin 0_c 1_c
45	43, 44	syl 15	. . . . . . 7 1_c S_fin 0_c T_fin S_fin 0_c 1_c
46	38, 45	mpbiri 224	. . . . . 6 1_c S_fin 0_c T_fin
47	40, 46	syl 15	. . . . 5 S_fin 0_c S_fin 0_c T_fin
48	47	ax-gen 1546	. . . 4 S_fin 0_c S_fin 0_c T_fin
49		df-sfin 4447	. . . . . . . . . 10 S_fin 1_c 1_c Nn $/\$ Nn $/\$ ₁ 1_c $/\$
50	49	simp3bi 972	. . . . . . . . 9 S_fin 1_c ₁ 1_c $/\$
51	50	3ad2ant3 978	. . . . . . . 8 Nn $/\$ S_fin S_fin T_fin T_fin $/\$ S_fin 1_c ₁ 1_c $/\$
52		sfindbl 4531	. . . . . . . . . . . . 13 Nn $/\$ ₁ 1_c Nn S_fin $/\$ S_fin 1_c
53	52	3ad2antl1 1117	. . . . . . . . . . . 12 Nn $/\$ S_fin S_fin T_fin T_fin $/\$ S_fin 1_c $/\$ ₁ 1_c Nn S_fin $/\$ S_fin 1_c
54		sfineq2 4528	. . . . . . . . . . . . . . . . . . . . . 22 S_fin S_fin
55		tfineq 4489	. . . . . . . . . . . . . . . . . . . . . . 23 T_fin T_fin
56		sfineq2 4528	. . . . . . . . . . . . . . . . . . . . . . 23 T_fin T_fin S_fin T_fin T_fin S_fin T_fin T_fin
57	55, 56	syl 15	. . . . . . . . . . . . . . . . . . . . . 22 S_fin T_fin T_fin S_fin T_fin T_fin
58	54, 57	imbi12d 311	. . . . . . . . . . . . . . . . . . . . 21 S_fin S_fin T_fin T_fin S_fin S_fin T_fin T_fin
59	58	spv 1998	. . . . . . . . . . . . . . . . . . . 20 S_fin S_fin T_fin T_fin S_fin S_fin T_fin T_fin
60		simprrl 740	. . . . . . . . . . . . . . . . . . . . . 22 S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c S_fin
61	60	adantl 452	. . . . . . . . . . . . . . . . . . . . 21 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c S_fin
62		simplrl 736	. . . . . . . . . . . . . . . . . . . . . . . 24 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin S_fin 1_c
63		simprrr 741	. . . . . . . . . . . . . . . . . . . . . . . . 25 S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c S_fin 1_c
64	63	ad2antlr 707	. . . . . . . . . . . . . . . . . . . . . . . 24 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin S_fin 1_c
65		sfin112 4530	. . . . . . . . . . . . . . . . . . . . . . . 24 S_fin 1_c $/\$ S_fin 1_c
66	62, 64, 65	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . 23 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin
67		df-sfin 4447	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 S_fin 1_c 1_c Nn $/\$ Nn $/\$ ₁ 1_c $/\$
68	67	simp3bi 972	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 S_fin 1_c ₁ 1_c $/\$
69	64, 68	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin ₁ 1_c $/\$
70		simp2 956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ ₁ 1_c S_fin T_fin T_fin
71		df-sfin 4447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 S_fin T_fin T_fin T_fin Nn $/\$ T_fin Nn $/\$ ₁ T_fin $/\$ T_fin
72	71	simp1bi 970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 S_fin T_fin T_fin T_fin Nn
73	70, 72	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ ₁ 1_c T_fin Nn
74		simp1l 979	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ ₁ 1_c Nn
75		peano2 4404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn 1_c Nn
76	74, 75	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ ₁ 1_c 1_c Nn
77		simp3 957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ ₁ 1_c ₁ 1_c
78		tfinpw1 4495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 1_c Nn $/\$ ₁ 1_c ₁ ₁ T_fin 1_c
79	76, 77, 78	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ ₁ 1_c ₁ ₁ T_fin 1_c
80		ne0i 3557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ₁ 1_c 1_c
81	80	3ad2ant3 978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ ₁ 1_c 1_c
82		tfinsuc 4499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Nn $/\$ 1_c T_fin 1_c T_fin 1_c
83	74, 81, 82	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ ₁ 1_c T_fin 1_c T_fin 1_c
84	79, 83	eleqtrd 2429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ ₁ 1_c ₁ ₁ T_fin 1_c
85		sfindbl 4531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 T_fin Nn $/\$ ₁ ₁ T_fin 1_c Nn S_fin T_fin $/\$ S_fin T_fin 1_c
86	73, 84, 85	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ ₁ 1_c Nn S_fin T_fin $/\$ S_fin T_fin 1_c
87		simp2 956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ S_fin T_fin $/\$ S_fin T_fin 1_c S_fin T_fin T_fin
88		simp3l 983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ S_fin T_fin $/\$ S_fin T_fin 1_c S_fin T_fin
89		sfin112 4530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 S_fin T_fin T_fin $/\$ S_fin T_fin T_fin
90	87, 88, 89	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ S_fin T_fin $/\$ S_fin T_fin 1_c T_fin
91		addceq12 4386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 T_fin $/\$ T_fin T_fin T_fin
92	91	anidms 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 T_fin T_fin T_fin
93		sfineq2 4528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 T_fin T_fin S_fin T_fin 1_c T_fin T_fin S_fin T_fin 1_c
94	92, 93	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 T_fin S_fin T_fin 1_c T_fin T_fin S_fin T_fin 1_c
95	94	biimprcd 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 S_fin T_fin 1_c T_fin S_fin T_fin 1_c T_fin T_fin
96	95	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 S_fin T_fin $/\$ S_fin T_fin 1_c T_fin S_fin T_fin 1_c T_fin T_fin
97	96	3ad2ant3 978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ S_fin T_fin $/\$ S_fin T_fin 1_c T_fin S_fin T_fin 1_c T_fin T_fin
98	90, 97	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ S_fin T_fin $/\$ S_fin T_fin 1_c S_fin T_fin 1_c T_fin T_fin
99	98	3expia 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin S_fin T_fin $/\$ S_fin T_fin 1_c S_fin T_fin 1_c T_fin T_fin
100	99	rexlimdvw 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin Nn S_fin T_fin $/\$ S_fin T_fin 1_c S_fin T_fin 1_c T_fin T_fin
101	100	3adant3 975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ ₁ 1_c Nn S_fin T_fin $/\$ S_fin T_fin 1_c S_fin T_fin 1_c T_fin T_fin
102	86, 101	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin $/\$ ₁ 1_c S_fin T_fin 1_c T_fin T_fin
103	102	3expia 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin ₁ 1_c S_fin T_fin 1_c T_fin T_fin
104	103	adantrd 454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin ₁ 1_c $/\$ S_fin T_fin 1_c T_fin T_fin
105	104	exlimdv 1636	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin ₁ 1_c $/\$ S_fin T_fin 1_c T_fin T_fin
106	69, 105	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin S_fin T_fin 1_c T_fin T_fin
107		simpll 730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin Nn
108	80	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ₁ 1_c $/\$ 1_c
109	108	exlimiv 1634	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ₁ 1_c $/\$ 1_c
110	64, 68, 109	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin 1_c
111	107, 110, 82	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin T_fin 1_c T_fin 1_c
112		simprrl 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c Nn
113	112	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin Nn
114		ne0i 3557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115	114	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ₁ 1_c $/\$
116	115	exlimiv 1634	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ₁ 1_c $/\$
117	64, 68, 116	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin
118		tfindi 4497	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn $/\$ Nn $/\$ T_fin T_fin T_fin
119	113, 113, 117, 118	syl3anc 1182	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin T_fin T_fin T_fin
120		sfineq1 4527	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 T_fin 1_c T_fin 1_c S_fin T_fin 1_c T_fin S_fin T_fin 1_c T_fin
121		sfineq2 4528	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 T_fin T_fin T_fin S_fin T_fin 1_c T_fin S_fin T_fin 1_c T_fin T_fin
122	120, 121	sylan9bb 680	. . . . . . . . . . . . . . . . . . . . . . . . . 26 T_fin 1_c T_fin 1_c $/\$ T_fin T_fin T_fin S_fin T_fin 1_c T_fin S_fin T_fin 1_c T_fin T_fin
123	111, 119, 122	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . 25 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin S_fin T_fin 1_c T_fin S_fin T_fin 1_c T_fin T_fin
124	106, 123	mpbird 223	. . . . . . . . . . . . . . . . . . . . . . . 24 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin S_fin T_fin 1_c T_fin
125		tfineq 4489	. . . . . . . . . . . . . . . . . . . . . . . . . 26 T_fin T_fin
126		sfineq2 4528	. . . . . . . . . . . . . . . . . . . . . . . . . 26 T_fin T_fin S_fin T_fin 1_c T_fin S_fin T_fin 1_c T_fin
127	125, 126	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 S_fin T_fin 1_c T_fin S_fin T_fin 1_c T_fin
128	127	biimprcd 216	. . . . . . . . . . . . . . . . . . . . . . . 24 S_fin T_fin 1_c T_fin S_fin T_fin 1_c T_fin
129	124, 128	syl 15	. . . . . . . . . . . . . . . . . . . . . . 23 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin S_fin T_fin 1_c T_fin
130	66, 129	mpd 14	. . . . . . . . . . . . . . . . . . . . . 22 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c $/\$ S_fin T_fin T_fin S_fin T_fin 1_c T_fin
131	130	ex 423	. . . . . . . . . . . . . . . . . . . . 21 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c S_fin T_fin T_fin S_fin T_fin 1_c T_fin
132	61, 131	embantd 50	. . . . . . . . . . . . . . . . . . . 20 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c S_fin S_fin T_fin T_fin S_fin T_fin 1_c T_fin
133	59, 132	syl5 28	. . . . . . . . . . . . . . . . . . 19 Nn $/\$ S_fin 1_c $/\$ Nn $/\$ S_fin $/\$ S_fin 1_c S_fin S_fin T_fin T_fin S_fin T_fin 1_c T_fin
134	133	exp32 588	. . . . . . . . . . . . . . . . . 18 Nn S_fin 1_c Nn $/\$ S_fin $/\$ S_fin 1_c S_fin S_fin T_fin T_fin S_fin T_fin 1_c T_fin
135	134	com34 77	. . . . . . . . . . . . . . . . 17 Nn S_fin 1_c S_fin S_fin T_fin T_fin Nn $/\$ S_fin $/\$ S_fin 1_c S_fin T_fin 1_c T_fin
136	135	com23 72	. . . . . . . . . . . . . . . 16 Nn S_fin S_fin T_fin T_fin S_fin 1_c Nn $/\$ S_fin $/\$ S_fin 1_c S_fin T_fin 1_c T_fin
137	136	3imp 1145	. . . . . . . . . . . . . . 15 Nn $/\$ S_fin S_fin T_fin T_fin $/\$ S_fin 1_c Nn $/\$ S_fin $/\$ S_fin 1_c S_fin T_fin 1_c T_fin
138	137	exp3a 425	. . . . . . . . . . . . . 14 Nn $/\$ S_fin S_fin T_fin T_fin $/\$ S_fin 1_c Nn S_fin $/\$ S_fin 1_c S_fin T_fin 1_c T_fin
139	138	rexlimdv 2738	. . . . . . . . . . . . 13 Nn $/\$ S_fin S_fin T_fin T_fin $/\$ S_fin 1_c Nn S_fin $/\$ S_fin 1_c S_fin T_fin 1_c T_fin
140	139	adantr 451	. . . . . . . . . . . 12 Nn $/\$ S_fin S_fin T_fin T_fin $/\$ S_fin 1_c $/\$ ₁ 1_c Nn S_fin $/\$ S_fin 1_c S_fin T_fin 1_c T_fin
141	53, 140	mpd 14	. . . . . . . . . . 11 Nn $/\$ S_fin S_fin T_fin T_fin $/\$ S_fin 1_c $/\$ ₁ 1_c S_fin T_fin 1_c T_fin
142	141	ex 423	. . . . . . . . . 10 Nn $/\$ S_fin S_fin T_fin T_fin $/\$ S_fin 1_c ₁ 1_c S_fin T_fin 1_c T_fin
143	142	adantrd 454	. . . . . . . . 9 Nn $/\$ S_fin S_fin T_fin T_fin $/\$ S_fin 1_c ₁ 1_c $/\$ S_fin T_fin 1_c T_fin
144	143	exlimdv 1636	. . . . . . . 8 Nn $/\$ S_fin S_fin T_fin T_fin $/\$ S_fin 1_c ₁ 1_c $/\$ S_fin T_fin 1_c T_fin
145	51, 144	mpd 14	. . . . . . 7 Nn $/\$ S_fin S_fin T_fin T_fin $/\$ S_fin 1_c S_fin T_fin 1_c T_fin
146	145	3expia 1153	. . . . . 6 Nn $/\$ S_fin S_fin T_fin T_fin S_fin 1_c S_fin T_fin 1_c T_fin
147	146	alrimiv 1631	. . . . 5 Nn $/\$ S_fin S_fin T_fin T_fin S_fin 1_c S_fin T_fin 1_c T_fin
148	147	ex 423	. . . 4 Nn S_fin S_fin T_fin T_fin S_fin 1_c S_fin T_fin 1_c T_fin
149	4, 12, 25, 31, 37, 48, 148	finds 4412	. . 3 Nn S_fin S_fin T_fin T_fin
150		sfineq2 4528	. . . . 5 S_fin S_fin
151		tfineq 4489	. . . . . 6 T_fin T_fin
152		sfineq2 4528	. . . . . 6 T_fin T_fin S_fin T_fin T_fin S_fin T_fin T_fin
153	151, 152	syl 15	. . . . 5 S_fin T_fin T_fin S_fin T_fin T_fin
154	150, 153	imbi12d 311	. . . 4 S_fin S_fin T_fin T_fin S_fin S_fin T_fin T_fin
155	154	spcgv 2940	. . 3 Nn S_fin S_fin T_fin T_fin S_fin S_fin T_fin T_fin
156	149, 155	mpan9 455	. 2 Nn $/\$ Nn S_fin S_fin T_fin T_fin
157	3, 156	mpcom 32	1 S_fin S_fin T_fin T_fin

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 176 $/\$ wa 358 $/\$ w3a 934

wal 1540

wex 1541

wceq 1642

wcel 1710

wne 2517

wrex 2616

c0 3551

cpw 3723 1_cc1c 4135

₁ cpw1 4136 Nn cnnc 4374 0_cc0c 4375

cplc 4376 T_fin ctfin 4436 S_fin wsfin 4439

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-13 1712 ax-14 1714 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-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-eu 2208 df-mo 2209 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-reu 2622 df-rmo 2623 df-rab 2624 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-idk 4196 df-iota 4340 df-0c 4378 df-addc 4379 df-nnc 4380 df-tfin 4444 df-sfin 4447

This theorem is referenced by: t1csfin1c 4546 vfinspsslem1 4551 vfinspclt 4553

W3C validator