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

Theorem sfintfin 4532
Description: If two numbers obey Sfin, then do their T raisings. Theorem X.1.45 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)
Assertion
Ref Expression
sfintfin Sfin Sfin Tfin Tfin

Proof of Theorem sfintfin
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sfin 4446 . . 3 Sfin Nn Nn 1
2 3simpa 952 . . 3 Nn Nn 1 Nn Nn
31, 2sylbi 187 . 2 Sfin Nn Nn
4 sfintfinlem1 4531 . . . 4 Sfin Sfin Tfin Tfin
5 sfineq1 4526 . . . . . 6 0c Sfin Sfin 0c
6 tfineq 4488 . . . . . . . 8 0c Tfin Tfin 0c
7 tfin0c 4497 . . . . . . . 8 Tfin 0c 0c
86, 7syl6eq 2401 . . . . . . 7 0c Tfin 0c
9 sfineq1 4526 . . . . . . 7 Tfin 0c Sfin Tfin Tfin Sfin 0c Tfin
108, 9syl 15 . . . . . 6 0c Sfin Tfin Tfin Sfin 0c Tfin
115, 10imbi12d 311 . . . . 5 0c Sfin Sfin Tfin Tfin Sfin 0c Sfin 0c Tfin
1211albidv 1625 . . . 4 0c Sfin Sfin Tfin Tfin Sfin 0c Sfin 0c Tfin
13 sfineq1 4526 . . . . . . 7 Sfin Sfin
14 tfineq 4488 . . . . . . . 8 Tfin Tfin
15 sfineq1 4526 . . . . . . . 8 Tfin Tfin Sfin Tfin Tfin Sfin Tfin Tfin
1614, 15syl 15 . . . . . . 7 Sfin Tfin Tfin Sfin Tfin Tfin
1713, 16imbi12d 311 . . . . . 6 Sfin Sfin Tfin Tfin Sfin Sfin Tfin Tfin
1817albidv 1625 . . . . 5 Sfin Sfin Tfin Tfin Sfin Sfin Tfin Tfin
19 sfineq2 4527 . . . . . . 7 Sfin Sfin
20 tfineq 4488 . . . . . . . 8 Tfin Tfin
21 sfineq2 4527 . . . . . . . 8 Tfin Tfin Sfin Tfin Tfin Sfin Tfin Tfin
2220, 21syl 15 . . . . . . 7 Sfin Tfin Tfin Sfin Tfin Tfin
2319, 22imbi12d 311 . . . . . 6 Sfin Sfin Tfin Tfin Sfin Sfin Tfin Tfin
2423cbvalv 2002 . . . . 5 Sfin Sfin Tfin Tfin Sfin Sfin Tfin Tfin
2518, 24syl6bb 252 . . . 4 Sfin Sfin Tfin Tfin Sfin Sfin Tfin Tfin
26 sfineq1 4526 . . . . . 6 1c Sfin Sfin 1c
27 tfineq 4488 . . . . . . 7 1c Tfin Tfin 1c
28 sfineq1 4526 . . . . . . 7 Tfin Tfin 1c Sfin Tfin Tfin Sfin Tfin 1c Tfin
2927, 28syl 15 . . . . . 6 1c Sfin Tfin Tfin Sfin Tfin 1c Tfin
3026, 29imbi12d 311 . . . . 5 1c Sfin Sfin Tfin Tfin Sfin 1c Sfin Tfin 1c Tfin
3130albidv 1625 . . . 4 1c Sfin Sfin Tfin Tfin Sfin 1c Sfin Tfin 1c Tfin
32 sfineq1 4526 . . . . . 6 Sfin Sfin
33 tfineq 4488 . . . . . . 7 Tfin Tfin
34 sfineq1 4526 . . . . . . 7 Tfin Tfin Sfin Tfin Tfin Sfin Tfin Tfin
3533, 34syl 15 . . . . . 6 Sfin Tfin Tfin Sfin Tfin Tfin
3632, 35imbi12d 311 . . . . 5 Sfin Sfin Tfin Tfin Sfin Sfin Tfin Tfin
3736albidv 1625 . . . 4 Sfin Sfin Tfin Tfin Sfin Sfin Tfin Tfin
38 sfin01 4528 . . . . . . 7 Sfin 0c 1c
39 sfin112 4529 . . . . . . 7 Sfin 0c Sfin 0c 1c 1c
4038, 39mpan2 652 . . . . . 6 Sfin 0c 1c
41 tfineq 4488 . . . . . . . . 9 1c Tfin Tfin 1c
42 tfin1c 4499 . . . . . . . . 9 Tfin 1c 1c
4341, 42syl6eq 2401 . . . . . . . 8 1c Tfin 1c
44 sfineq2 4527 . . . . . . . 8 Tfin 1c Sfin 0c Tfin Sfin 0c 1c
4543, 44syl 15 . . . . . . 7 1c Sfin 0c Tfin Sfin 0c 1c
4638, 45mpbiri 224 . . . . . 6 1c Sfin 0c Tfin
4740, 46syl 15 . . . . 5 Sfin 0c Sfin 0c Tfin
4847ax-gen 1546 . . . 4 Sfin 0c Sfin 0c Tfin
49 df-sfin 4446 . . . . . . . . . 10 Sfin 1c 1c Nn Nn 1 1c
5049simp3bi 972 . . . . . . . . 9 Sfin 1c 1 1c
51503ad2ant3 978 . . . . . . . 8 Nn Sfin Sfin Tfin Tfin Sfin 1c 1 1c
52 sfindbl 4530 . . . . . . . . . . . . 13 Nn 1 1c Nn Sfin Sfin 1c
53523ad2antl1 1117 . . . . . . . . . . . 12 Nn Sfin Sfin Tfin Tfin Sfin 1c 1 1c Nn Sfin Sfin 1c
54 sfineq2 4527 . . . . . . . . . . . . . . . . . . . . . 22 Sfin Sfin
55 tfineq 4488 . . . . . . . . . . . . . . . . . . . . . . 23 Tfin Tfin
56 sfineq2 4527 . . . . . . . . . . . . . . . . . . . . . . 23 Tfin Tfin Sfin Tfin Tfin Sfin Tfin Tfin
5755, 56syl 15 . . . . . . . . . . . . . . . . . . . . . 22 Sfin Tfin Tfin Sfin Tfin Tfin
5854, 57imbi12d 311 . . . . . . . . . . . . . . . . . . . . 21 Sfin Sfin Tfin Tfin Sfin Sfin Tfin Tfin
5958spv 1998 . . . . . . . . . . . . . . . . . . . 20 Sfin Sfin Tfin Tfin Sfin Sfin Tfin Tfin
60 simprrl 740 . . . . . . . . . . . . . . . . . . . . . 22 Sfin 1c Nn Sfin Sfin 1c Sfin
6160adantl 452 . . . . . . . . . . . . . . . . . . . . 21 Nn Sfin 1c Nn Sfin Sfin 1c Sfin
62 simplrl 736 . . . . . . . . . . . . . . . . . . . . . . . 24 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin 1c
63 simprrr 741 . . . . . . . . . . . . . . . . . . . . . . . . 25 Sfin 1c Nn Sfin Sfin 1c Sfin 1c
6463ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . 24 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin 1c
65 sfin112 4529 . . . . . . . . . . . . . . . . . . . . . . . 24 Sfin 1c Sfin 1c
6662, 64, 65syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin
67 df-sfin 4446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Sfin 1c 1c Nn Nn 1 1c
6867simp3bi 972 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Sfin 1c 1 1c
6964, 68syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c
70 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c Sfin Tfin Tfin
71 df-sfin 4446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Sfin Tfin Tfin Tfin Nn Tfin Nn 1 Tfin Tfin
7271simp1bi 970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Sfin Tfin Tfin Tfin Nn
7370, 72syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c Tfin Nn
74 simp1l 979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c Nn
75 peano2 4403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn 1c Nn
7674, 75syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c 1c Nn
77 simp3 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c 1 1c
78 tfinpw1 4494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 1c Nn 1 1c 1 1 Tfin 1c
7976, 77, 78syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c 1 1 Tfin 1c
80 ne0i 3556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1 1c 1c
81803ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c 1c
82 tfinsuc 4498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Nn 1c Tfin 1c Tfin 1c
8374, 81, 82syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c Tfin 1c Tfin 1c
8479, 83eleqtrd 2429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c 1 1 Tfin 1c
85 sfindbl 4530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Tfin Nn 1 1 Tfin 1c Nn Sfin Tfin Sfin Tfin 1c
8673, 84, 85syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c Nn Sfin Tfin Sfin Tfin 1c
87 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin Tfin Sfin Tfin 1c Sfin Tfin Tfin
88 simp3l 983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin Tfin Sfin Tfin 1c Sfin Tfin
89 sfin112 4529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Sfin Tfin Tfin Sfin Tfin Tfin
9087, 88, 89syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin Tfin Sfin Tfin 1c Tfin
91 addceq12 4385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Tfin Tfin Tfin Tfin
9291anidms 626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Tfin Tfin Tfin
93 sfineq2 4527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Tfin Tfin Sfin Tfin 1c Tfin Tfin Sfin Tfin 1c
9492, 93syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Tfin Sfin Tfin 1c Tfin Tfin Sfin Tfin 1c
9594biimprcd 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Sfin Tfin 1c Tfin Sfin Tfin 1c Tfin Tfin
9695adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Sfin Tfin Sfin Tfin 1c Tfin Sfin Tfin 1c Tfin Tfin
97963ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin Tfin Sfin Tfin 1c Tfin Sfin Tfin 1c Tfin Tfin
9890, 97mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin Tfin Sfin Tfin 1c Sfin Tfin 1c Tfin Tfin
99983expia 1153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin Tfin Sfin Tfin 1c Sfin Tfin 1c Tfin Tfin
10099rexlimdvw 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Nn Sfin Tfin Sfin Tfin 1c Sfin Tfin 1c Tfin Tfin
1011003adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c Nn Sfin Tfin Sfin Tfin 1c Sfin Tfin 1c Tfin Tfin
10286, 101mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c Sfin Tfin 1c Tfin Tfin
1031023expia 1153 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c Sfin Tfin 1c Tfin Tfin
104103adantrd 454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c Sfin Tfin 1c Tfin Tfin
105104exlimdv 1636 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1 1c Sfin Tfin 1c Tfin Tfin
10669, 105mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin Tfin 1c Tfin Tfin
107 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Nn
10880adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 1c 1c
109108exlimiv 1634 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 1c 1c
11064, 68, 1093syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin 1c
111107, 110, 82syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Tfin 1c Tfin 1c
112 simprrl 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Nn Sfin 1c Nn Sfin Sfin 1c Nn
113112adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Nn
114 ne0i 3556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115114adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 1c
116115exlimiv 1634 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 1c
11764, 68, 1163syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin
118 tfindi 4496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn Nn Tfin Tfin Tfin
119113, 113, 117, 118syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Tfin Tfin Tfin
120 sfineq1 4526 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Tfin 1c Tfin 1c Sfin Tfin 1c Tfin Sfin Tfin 1c Tfin
121 sfineq2 4527 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Tfin Tfin Tfin Sfin Tfin 1c Tfin Sfin Tfin 1c Tfin Tfin
122120, 121sylan9bb 680 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Tfin 1c Tfin 1c Tfin Tfin Tfin Sfin Tfin 1c Tfin Sfin Tfin 1c Tfin Tfin
123111, 119, 122syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin Tfin 1c Tfin Sfin Tfin 1c Tfin Tfin
124106, 123mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . 24 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin Tfin 1c Tfin
125 tfineq 4488 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Tfin Tfin
126 sfineq2 4527 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Tfin Tfin Sfin Tfin 1c Tfin Sfin Tfin 1c Tfin
127125, 126syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 Sfin Tfin 1c Tfin Sfin Tfin 1c Tfin
128127biimprcd 216 . . . . . . . . . . . . . . . . . . . . . . . 24 Sfin Tfin 1c Tfin Sfin Tfin 1c Tfin
129124, 128syl 15 . . . . . . . . . . . . . . . . . . . . . . 23 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin Tfin 1c Tfin
13066, 129mpd 14 . . . . . . . . . . . . . . . . . . . . . 22 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin Tfin 1c Tfin
131130ex 423 . . . . . . . . . . . . . . . . . . . . 21 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Tfin Tfin Sfin Tfin 1c Tfin
13261, 131embantd 50 . . . . . . . . . . . . . . . . . . . 20 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Sfin Tfin Tfin Sfin Tfin 1c Tfin
13359, 132syl5 28 . . . . . . . . . . . . . . . . . . 19 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Sfin Tfin Tfin Sfin Tfin 1c Tfin
134133exp32 588 . . . . . . . . . . . . . . . . . 18 Nn Sfin 1c Nn Sfin Sfin 1c Sfin Sfin Tfin Tfin Sfin Tfin 1c Tfin
135134com34 77 . . . . . . . . . . . . . . . . 17 Nn Sfin 1c Sfin Sfin Tfin Tfin Nn Sfin Sfin 1c Sfin Tfin 1c Tfin
136135com23 72 . . . . . . . . . . . . . . . 16 Nn Sfin Sfin Tfin Tfin Sfin 1c Nn Sfin Sfin 1c Sfin Tfin 1c Tfin
1371363imp 1145 . . . . . . . . . . . . . . 15 Nn Sfin Sfin Tfin Tfin Sfin 1c Nn Sfin Sfin 1c Sfin Tfin 1c Tfin
138137exp3a 425 . . . . . . . . . . . . . 14 Nn Sfin Sfin Tfin Tfin Sfin 1c Nn Sfin Sfin 1c Sfin Tfin 1c Tfin
139138rexlimdv 2737 . . . . . . . . . . . . 13 Nn Sfin Sfin Tfin Tfin Sfin 1c Nn Sfin Sfin 1c Sfin Tfin 1c Tfin
140139adantr 451 . . . . . . . . . . . 12 Nn Sfin Sfin Tfin Tfin Sfin 1c 1 1c Nn Sfin Sfin 1c Sfin Tfin 1c Tfin
14153, 140mpd 14 . . . . . . . . . . 11 Nn Sfin Sfin Tfin Tfin Sfin 1c 1 1c Sfin Tfin 1c Tfin
142141ex 423 . . . . . . . . . 10 Nn Sfin Sfin Tfin Tfin Sfin 1c 1 1c Sfin Tfin 1c Tfin
143142adantrd 454 . . . . . . . . 9 Nn Sfin Sfin Tfin Tfin Sfin 1c 1 1c Sfin Tfin 1c Tfin
144143exlimdv 1636 . . . . . . . 8 Nn Sfin Sfin Tfin Tfin Sfin 1c 1 1c Sfin Tfin 1c Tfin
14551, 144mpd 14 . . . . . . 7 Nn Sfin Sfin Tfin Tfin Sfin 1c Sfin Tfin 1c Tfin
1461453expia 1153 . . . . . 6 Nn Sfin Sfin Tfin Tfin Sfin 1c Sfin Tfin 1c Tfin
147146alrimiv 1631 . . . . 5 Nn Sfin Sfin Tfin Tfin Sfin 1c Sfin Tfin 1c Tfin
148147ex 423 . . . 4 Nn Sfin Sfin Tfin Tfin Sfin 1c Sfin Tfin 1c Tfin
1494, 12, 25, 31, 37, 48, 148finds 4411 . . 3 Nn Sfin Sfin Tfin Tfin
150 sfineq2 4527 . . . . 5 Sfin Sfin
151 tfineq 4488 . . . . . 6 Tfin Tfin
152 sfineq2 4527 . . . . . 6 Tfin Tfin Sfin Tfin Tfin Sfin Tfin Tfin
153151, 152syl 15 . . . . 5 Sfin Tfin Tfin Sfin Tfin Tfin
154150, 153imbi12d 311 . . . 4 Sfin Sfin Tfin Tfin Sfin Sfin Tfin Tfin
155154spcgv 2939 . . 3 Nn Sfin Sfin Tfin Tfin Sfin Sfin Tfin Tfin
156149, 155mpan9 455 . 2 Nn Nn Sfin Sfin Tfin Tfin
1573, 156mpcom 32 1 Sfin Sfin Tfin Tfin
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 2516  wrex 2615  c0 3550  cpw 3722  1cc1c 4134  1 cpw1 4135   Nn cnnc 4373  0cc0c 4374   cplc 4375   Tfin ctfin 4435   Sfin wsfin 4438
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 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
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 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-tfin 4443  df-sfin 4446
This theorem is referenced by:  t1csfin1c  4545  vfinspsslem1  4550  vfinspclt  4552
  Copyright terms: Public domain W3C validator