New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  sfintfin GIF 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 (M, N) → Sfin ( Tfin M, Tfin N))

Proof of Theorem sfintfin
Dummy variables a k m n p q are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sfin 4446 . . 3 ( Sfin (M, N) ↔ (M Nn N Nn a(1a M a N)))
2 3simpa 952 . . 3 ((M Nn N Nn a(1a M a N)) → (M Nn N Nn ))
31, 2sylbi 187 . 2 ( Sfin (M, N) → (M Nn N Nn ))
4 sfintfinlem1 4531 . . . 4 {k n( Sfin (k, n) → Sfin ( Tfin k, Tfin n))} V
5 sfineq1 4526 . . . . . 6 (k = 0c → ( Sfin (k, n) ↔ Sfin (0c, n)))
6 tfineq 4488 . . . . . . . 8 (k = 0cTfin k = Tfin 0c)
7 tfin0c 4497 . . . . . . . 8 Tfin 0c = 0c
86, 7syl6eq 2401 . . . . . . 7 (k = 0cTfin k = 0c)
9 sfineq1 4526 . . . . . . 7 ( Tfin k = 0c → ( Sfin ( Tfin k, Tfin n) ↔ Sfin (0c, Tfin n)))
108, 9syl 15 . . . . . 6 (k = 0c → ( Sfin ( Tfin k, Tfin n) ↔ Sfin (0c, Tfin n)))
115, 10imbi12d 311 . . . . 5 (k = 0c → (( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ ( Sfin (0c, n) → Sfin (0c, Tfin n))))
1211albidv 1625 . . . 4 (k = 0c → (n( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ n( Sfin (0c, n) → Sfin (0c, Tfin n))))
13 sfineq1 4526 . . . . . . 7 (k = m → ( Sfin (k, n) ↔ Sfin (m, n)))
14 tfineq 4488 . . . . . . . 8 (k = mTfin k = Tfin m)
15 sfineq1 4526 . . . . . . . 8 ( Tfin k = Tfin m → ( Sfin ( Tfin k, Tfin n) ↔ Sfin ( Tfin m, Tfin n)))
1614, 15syl 15 . . . . . . 7 (k = m → ( Sfin ( Tfin k, Tfin n) ↔ Sfin ( Tfin m, Tfin n)))
1713, 16imbi12d 311 . . . . . 6 (k = m → (( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ ( Sfin (m, n) → Sfin ( Tfin m, Tfin n))))
1817albidv 1625 . . . . 5 (k = m → (n( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ n( Sfin (m, n) → Sfin ( Tfin m, Tfin n))))
19 sfineq2 4527 . . . . . . 7 (n = p → ( Sfin (m, n) ↔ Sfin (m, p)))
20 tfineq 4488 . . . . . . . 8 (n = pTfin n = Tfin p)
21 sfineq2 4527 . . . . . . . 8 ( Tfin n = Tfin p → ( Sfin ( Tfin m, Tfin n) ↔ Sfin ( Tfin m, Tfin p)))
2220, 21syl 15 . . . . . . 7 (n = p → ( Sfin ( Tfin m, Tfin n) ↔ Sfin ( Tfin m, Tfin p)))
2319, 22imbi12d 311 . . . . . 6 (n = p → (( Sfin (m, n) → Sfin ( Tfin m, Tfin n)) ↔ ( Sfin (m, p) → Sfin ( Tfin m, Tfin p))))
2423cbvalv 2002 . . . . 5 (n( Sfin (m, n) → Sfin ( Tfin m, Tfin n)) ↔ p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)))
2518, 24syl6bb 252 . . . 4 (k = m → (n( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ p( Sfin (m, p) → Sfin ( Tfin m, Tfin p))))
26 sfineq1 4526 . . . . . 6 (k = (m +c 1c) → ( Sfin (k, n) ↔ Sfin ((m +c 1c), n)))
27 tfineq 4488 . . . . . . 7 (k = (m +c 1c) → Tfin k = Tfin (m +c 1c))
28 sfineq1 4526 . . . . . . 7 ( Tfin k = Tfin (m +c 1c) → ( Sfin ( Tfin k, Tfin n) ↔ Sfin ( Tfin (m +c 1c), Tfin n)))
2927, 28syl 15 . . . . . 6 (k = (m +c 1c) → ( Sfin ( Tfin k, Tfin n) ↔ Sfin ( Tfin (m +c 1c), Tfin n)))
3026, 29imbi12d 311 . . . . 5 (k = (m +c 1c) → (( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ ( Sfin ((m +c 1c), n) → Sfin ( Tfin (m +c 1c), Tfin n))))
3130albidv 1625 . . . 4 (k = (m +c 1c) → (n( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ n( Sfin ((m +c 1c), n) → Sfin ( Tfin (m +c 1c), Tfin n))))
32 sfineq1 4526 . . . . . 6 (k = M → ( Sfin (k, n) ↔ Sfin (M, n)))
33 tfineq 4488 . . . . . . 7 (k = MTfin k = Tfin M)
34 sfineq1 4526 . . . . . . 7 ( Tfin k = Tfin M → ( Sfin ( Tfin k, Tfin n) ↔ Sfin ( Tfin M, Tfin n)))
3533, 34syl 15 . . . . . 6 (k = M → ( Sfin ( Tfin k, Tfin n) ↔ Sfin ( Tfin M, Tfin n)))
3632, 35imbi12d 311 . . . . 5 (k = M → (( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ ( Sfin (M, n) → Sfin ( Tfin M, Tfin n))))
3736albidv 1625 . . . 4 (k = M → (n( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ n( Sfin (M, n) → Sfin ( Tfin M, Tfin n))))
38 sfin01 4528 . . . . . . 7 Sfin (0c, 1c)
39 sfin112 4529 . . . . . . 7 (( Sfin (0c, n) Sfin (0c, 1c)) → n = 1c)
4038, 39mpan2 652 . . . . . 6 ( Sfin (0c, n) → n = 1c)
41 tfineq 4488 . . . . . . . . 9 (n = 1cTfin n = Tfin 1c)
42 tfin1c 4499 . . . . . . . . 9 Tfin 1c = 1c
4341, 42syl6eq 2401 . . . . . . . 8 (n = 1cTfin n = 1c)
44 sfineq2 4527 . . . . . . . 8 ( Tfin n = 1c → ( Sfin (0c, Tfin n) ↔ Sfin (0c, 1c)))
4543, 44syl 15 . . . . . . 7 (n = 1c → ( Sfin (0c, Tfin n) ↔ Sfin (0c, 1c)))
4638, 45mpbiri 224 . . . . . 6 (n = 1cSfin (0c, Tfin n))
4740, 46syl 15 . . . . 5 ( Sfin (0c, n) → Sfin (0c, Tfin n))
4847ax-gen 1546 . . . 4 n( Sfin (0c, n) → Sfin (0c, Tfin n))
49 df-sfin 4446 . . . . . . . . . 10 ( Sfin ((m +c 1c), n) ↔ ((m +c 1c) Nn n Nn a(1a (m +c 1c) a n)))
5049simp3bi 972 . . . . . . . . 9 ( Sfin ((m +c 1c), n) → a(1a (m +c 1c) a n))
51503ad2ant3 978 . . . . . . . 8 ((m Nn p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) Sfin ((m +c 1c), n)) → a(1a (m +c 1c) a n))
52 sfindbl 4530 . . . . . . . . . . . . 13 ((m Nn 1a (m +c 1c)) → q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q))))
53523ad2antl1 1117 . . . . . . . . . . . 12 (((m Nn p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) Sfin ((m +c 1c), n)) 1a (m +c 1c)) → q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q))))
54 sfineq2 4527 . . . . . . . . . . . . . . . . . . . . . 22 (p = q → ( Sfin (m, p) ↔ Sfin (m, q)))
55 tfineq 4488 . . . . . . . . . . . . . . . . . . . . . . 23 (p = qTfin p = Tfin q)
56 sfineq2 4527 . . . . . . . . . . . . . . . . . . . . . . 23 ( Tfin p = Tfin q → ( Sfin ( Tfin m, Tfin p) ↔ Sfin ( Tfin m, Tfin q)))
5755, 56syl 15 . . . . . . . . . . . . . . . . . . . . . 22 (p = q → ( Sfin ( Tfin m, Tfin p) ↔ Sfin ( Tfin m, Tfin q)))
5854, 57imbi12d 311 . . . . . . . . . . . . . . . . . . . . 21 (p = q → (( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) ↔ ( Sfin (m, q) → Sfin ( Tfin m, Tfin q))))
5958spv 1998 . . . . . . . . . . . . . . . . . . . 20 (p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) → ( Sfin (m, q) → Sfin ( Tfin m, Tfin q)))
60 simprrl 740 . . . . . . . . . . . . . . . . . . . . . 22 (( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q))))) → Sfin (m, q))
6160adantl 452 . . . . . . . . . . . . . . . . . . . . 21 ((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) → Sfin (m, q))
62 simplrl 736 . . . . . . . . . . . . . . . . . . . . . . . 24 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → Sfin ((m +c 1c), n))
63 simprrr 741 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q))))) → Sfin ((m +c 1c), (q +c q)))
6463ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . 24 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → Sfin ((m +c 1c), (q +c q)))
65 sfin112 4529 . . . . . . . . . . . . . . . . . . . . . . . 24 (( Sfin ((m +c 1c), n) Sfin ((m +c 1c), (q +c q))) → n = (q +c q))
6662, 64, 65syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → n = (q +c q))
67 df-sfin 4446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( Sfin ((m +c 1c), (q +c q)) ↔ ((m +c 1c) Nn (q +c q) Nn a(1a (m +c 1c) a (q +c q))))
6867simp3bi 972 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( Sfin ((m +c 1c), (q +c q)) → a(1a (m +c 1c) a (q +c q)))
6964, 68syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → a(1a (m +c 1c) a (q +c q)))
70 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) 1a (m +c 1c)) → Sfin ( Tfin m, Tfin q))
71 df-sfin 4446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( Sfin ( Tfin m, Tfin q) ↔ ( Tfin m Nn Tfin q Nn a(1a Tfin m a Tfin q)))
7271simp1bi 970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( Sfin ( Tfin m, Tfin q) → Tfin m Nn )
7370, 72syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) 1a (m +c 1c)) → Tfin m Nn )
74 simp1l 979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) 1a (m +c 1c)) → m Nn )
75 peano2 4403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (m Nn → (m +c 1c) Nn )
7674, 75syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) 1a (m +c 1c)) → (m +c 1c) Nn )
77 simp3 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) 1a (m +c 1c)) → 1a (m +c 1c))
78 tfinpw1 4494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((m +c 1c) Nn 1a (m +c 1c)) → 11a Tfin (m +c 1c))
7976, 77, 78syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) 1a (m +c 1c)) → 11a Tfin (m +c 1c))
80 ne0i 3556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (1a (m +c 1c) → (m +c 1c) ≠ )
81803ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) 1a (m +c 1c)) → (m +c 1c) ≠ )
82 tfinsuc 4498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((m Nn (m +c 1c) ≠ ) → Tfin (m +c 1c) = ( Tfin m +c 1c))
8374, 81, 82syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) 1a (m +c 1c)) → Tfin (m +c 1c) = ( Tfin m +c 1c))
8479, 83eleqtrd 2429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) 1a (m +c 1c)) → 11a ( Tfin m +c 1c))
85 sfindbl 4530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (( Tfin m Nn 11a ( Tfin m +c 1c)) → k Nn ( Sfin ( Tfin m, k) Sfin (( Tfin m +c 1c), (k +c k))))
8673, 84, 85syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) 1a (m +c 1c)) → k Nn ( Sfin ( Tfin m, k) Sfin (( Tfin m +c 1c), (k +c k))))
87 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) ( Sfin ( Tfin m, k) Sfin (( Tfin m +c 1c), (k +c k)))) → Sfin ( Tfin m, Tfin q))
88 simp3l 983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) ( Sfin ( Tfin m, k) Sfin (( Tfin m +c 1c), (k +c k)))) → Sfin ( Tfin m, k))
89 sfin112 4529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (( Sfin ( Tfin m, Tfin q) Sfin ( Tfin m, k)) → Tfin q = k)
9087, 88, 89syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) ( Sfin ( Tfin m, k) Sfin (( Tfin m +c 1c), (k +c k)))) → Tfin q = k)
91 addceq12 4385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (( Tfin q = k Tfin q = k) → ( Tfin q +c Tfin q) = (k +c k))
9291anidms 626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ( Tfin q = k → ( Tfin q +c Tfin q) = (k +c k))
93 sfineq2 4527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (( Tfin q +c Tfin q) = (k +c k) → ( Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q)) ↔ Sfin (( Tfin m +c 1c), (k +c k))))
9492, 93syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ( Tfin q = k → ( Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q)) ↔ Sfin (( Tfin m +c 1c), (k +c k))))
9594biimprcd 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ( Sfin (( Tfin m +c 1c), (k +c k)) → ( Tfin q = kSfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
9695adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (( Sfin ( Tfin m, k) Sfin (( Tfin m +c 1c), (k +c k))) → ( Tfin q = kSfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
97963ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) ( Sfin ( Tfin m, k) Sfin (( Tfin m +c 1c), (k +c k)))) → ( Tfin q = kSfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
9890, 97mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) ( Sfin ( Tfin m, k) Sfin (( Tfin m +c 1c), (k +c k)))) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q)))
99983expia 1153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → (( Sfin ( Tfin m, k) Sfin (( Tfin m +c 1c), (k +c k))) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
10099rexlimdvw 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → (k Nn ( Sfin ( Tfin m, k) Sfin (( Tfin m +c 1c), (k +c k))) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
1011003adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) 1a (m +c 1c)) → (k Nn ( Sfin ( Tfin m, k) Sfin (( Tfin m +c 1c), (k +c k))) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
10286, 101mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q) 1a (m +c 1c)) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q)))
1031023expia 1153 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → (1a (m +c 1c) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
104103adantrd 454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → ((1a (m +c 1c) a (q +c q)) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
105104exlimdv 1636 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → (a(1a (m +c 1c) a (q +c q)) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
10669, 105mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q)))
107 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → m Nn )
10880adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((1a (m +c 1c) a (q +c q)) → (m +c 1c) ≠ )
109108exlimiv 1634 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (a(1a (m +c 1c) a (q +c q)) → (m +c 1c) ≠ )
11064, 68, 1093syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → (m +c 1c) ≠ )
111107, 110, 82syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → Tfin (m +c 1c) = ( Tfin m +c 1c))
112 simprrl 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) → q Nn )
113112adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → q Nn )
114 ne0i 3556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (a (q +c q) → (q +c q) ≠ )
115114adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((1a (m +c 1c) a (q +c q)) → (q +c q) ≠ )
116115exlimiv 1634 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (a(1a (m +c 1c) a (q +c q)) → (q +c q) ≠ )
11764, 68, 1163syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → (q +c q) ≠ )
118 tfindi 4496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((q Nn q Nn (q +c q) ≠ ) → Tfin (q +c q) = ( Tfin q +c Tfin q))
119113, 113, 117, 118syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → Tfin (q +c q) = ( Tfin q +c Tfin q))
120 sfineq1 4526 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( Tfin (m +c 1c) = ( Tfin m +c 1c) → ( Sfin ( Tfin (m +c 1c), Tfin (q +c q)) ↔ Sfin (( Tfin m +c 1c), Tfin (q +c q))))
121 sfineq2 4527 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( Tfin (q +c q) = ( Tfin q +c Tfin q) → ( Sfin (( Tfin m +c 1c), Tfin (q +c q)) ↔ Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
122120, 121sylan9bb 680 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( Tfin (m +c 1c) = ( Tfin m +c 1c) Tfin (q +c q) = ( Tfin q +c Tfin q)) → ( Sfin ( Tfin (m +c 1c), Tfin (q +c q)) ↔ Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
123111, 119, 122syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → ( Sfin ( Tfin (m +c 1c), Tfin (q +c q)) ↔ Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
124106, 123mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . 24 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → Sfin ( Tfin (m +c 1c), Tfin (q +c q)))
125 tfineq 4488 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (n = (q +c q) → Tfin n = Tfin (q +c q))
126 sfineq2 4527 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( Tfin n = Tfin (q +c q) → ( Sfin ( Tfin (m +c 1c), Tfin n) ↔ Sfin ( Tfin (m +c 1c), Tfin (q +c q))))
127125, 126syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 (n = (q +c q) → ( Sfin ( Tfin (m +c 1c), Tfin n) ↔ Sfin ( Tfin (m +c 1c), Tfin (q +c q))))
128127biimprcd 216 . . . . . . . . . . . . . . . . . . . . . . . 24 ( Sfin ( Tfin (m +c 1c), Tfin (q +c q)) → (n = (q +c q) → Sfin ( Tfin (m +c 1c), Tfin n)))
129124, 128syl 15 . . . . . . . . . . . . . . . . . . . . . . 23 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → (n = (q +c q) → Sfin ( Tfin (m +c 1c), Tfin n)))
13066, 129mpd 14 . . . . . . . . . . . . . . . . . . . . . 22 (((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) Sfin ( Tfin m, Tfin q)) → Sfin ( Tfin (m +c 1c), Tfin n))
131130ex 423 . . . . . . . . . . . . . . . . . . . . 21 ((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) → ( Sfin ( Tfin m, Tfin q) → Sfin ( Tfin (m +c 1c), Tfin n)))
13261, 131embantd 50 . . . . . . . . . . . . . . . . . . . 20 ((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) → (( Sfin (m, q) → Sfin ( Tfin m, Tfin q)) → Sfin ( Tfin (m +c 1c), Tfin n)))
13359, 132syl5 28 . . . . . . . . . . . . . . . . . . 19 ((m Nn ( Sfin ((m +c 1c), n) (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))))) → (p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) → Sfin ( Tfin (m +c 1c), Tfin n)))
134133exp32 588 . . . . . . . . . . . . . . . . . 18 (m Nn → ( Sfin ((m +c 1c), n) → ((q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))) → (p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) → Sfin ( Tfin (m +c 1c), Tfin n)))))
135134com34 77 . . . . . . . . . . . . . . . . 17 (m Nn → ( Sfin ((m +c 1c), n) → (p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) → ((q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))) → Sfin ( Tfin (m +c 1c), Tfin n)))))
136135com23 72 . . . . . . . . . . . . . . . 16 (m Nn → (p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) → ( Sfin ((m +c 1c), n) → ((q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))) → Sfin ( Tfin (m +c 1c), Tfin n)))))
1371363imp 1145 . . . . . . . . . . . . . . 15 ((m Nn p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) Sfin ((m +c 1c), n)) → ((q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q)))) → Sfin ( Tfin (m +c 1c), Tfin n)))
138137exp3a 425 . . . . . . . . . . . . . 14 ((m Nn p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) Sfin ((m +c 1c), n)) → (q Nn → (( Sfin (m, q) Sfin ((m +c 1c), (q +c q))) → Sfin ( Tfin (m +c 1c), Tfin n))))
139138rexlimdv 2737 . . . . . . . . . . . . 13 ((m Nn p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) Sfin ((m +c 1c), n)) → (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q))) → Sfin ( Tfin (m +c 1c), Tfin n)))
140139adantr 451 . . . . . . . . . . . 12 (((m Nn p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) Sfin ((m +c 1c), n)) 1a (m +c 1c)) → (q Nn ( Sfin (m, q) Sfin ((m +c 1c), (q +c q))) → Sfin ( Tfin (m +c 1c), Tfin n)))
14153, 140mpd 14 . . . . . . . . . . 11 (((m Nn p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) Sfin ((m +c 1c), n)) 1a (m +c 1c)) → Sfin ( Tfin (m +c 1c), Tfin n))
142141ex 423 . . . . . . . . . 10 ((m Nn p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) Sfin ((m +c 1c), n)) → (1a (m +c 1c) → Sfin ( Tfin (m +c 1c), Tfin n)))
143142adantrd 454 . . . . . . . . 9 ((m Nn p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) Sfin ((m +c 1c), n)) → ((1a (m +c 1c) a n) → Sfin ( Tfin (m +c 1c), Tfin n)))
144143exlimdv 1636 . . . . . . . 8 ((m Nn p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) Sfin ((m +c 1c), n)) → (a(1a (m +c 1c) a n) → Sfin ( Tfin (m +c 1c), Tfin n)))
14551, 144mpd 14 . . . . . . 7 ((m Nn p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) Sfin ((m +c 1c), n)) → Sfin ( Tfin (m +c 1c), Tfin n))
1461453expia 1153 . . . . . 6 ((m Nn p( Sfin (m, p) → Sfin ( Tfin m, Tfin p))) → ( Sfin ((m +c 1c), n) → Sfin ( Tfin (m +c 1c), Tfin n)))
147146alrimiv 1631 . . . . 5 ((m Nn p( Sfin (m, p) → Sfin ( Tfin m, Tfin p))) → n( Sfin ((m +c 1c), n) → Sfin ( Tfin (m +c 1c), Tfin n)))
148147ex 423 . . . 4 (m Nn → (p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) → n( Sfin ((m +c 1c), n) → Sfin ( Tfin (m +c 1c), Tfin n))))
1494, 12, 25, 31, 37, 48, 148finds 4411 . . 3 (M Nnn( Sfin (M, n) → Sfin ( Tfin M, Tfin n)))
150 sfineq2 4527 . . . . 5 (n = N → ( Sfin (M, n) ↔ Sfin (M, N)))
151 tfineq 4488 . . . . . 6 (n = NTfin n = Tfin N)
152 sfineq2 4527 . . . . . 6 ( Tfin n = Tfin N → ( Sfin ( Tfin M, Tfin n) ↔ Sfin ( Tfin M, Tfin N)))
153151, 152syl 15 . . . . 5 (n = N → ( Sfin ( Tfin M, Tfin n) ↔ Sfin ( Tfin M, Tfin N)))
154150, 153imbi12d 311 . . . 4 (n = N → (( Sfin (M, n) → Sfin ( Tfin M, Tfin n)) ↔ ( Sfin (M, N) → Sfin ( Tfin M, Tfin N))))
155154spcgv 2939 . . 3 (N Nn → (n( Sfin (M, n) → Sfin ( Tfin M, Tfin n)) → ( Sfin (M, N) → Sfin ( Tfin M, Tfin N))))
156149, 155mpan9 455 . 2 ((M Nn N Nn ) → ( Sfin (M, N) → Sfin ( Tfin M, Tfin N)))
1573, 156mpcom 32 1 ( Sfin (M, N) → Sfin ( Tfin M, Tfin N))
 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  ℘1cpw1 4135   Nn cnnc 4373  0cc0c 4374   +c 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