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

Theorem sfinltfin 4535
Description: Ordering law for finite smaller than. Theorem X.1.47 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)
Assertion
Ref Expression
sfinltfin ((( Sfin (M, N) Sfin (P, Q)) M, P <fin ) → ⟪N, Q <fin )

Proof of Theorem sfinltfin
Dummy variables a b r s d g t x n u m 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 df-sfin 4446 . . 3 ( Sfin (P, Q) ↔ (P Nn Q Nn b(1b P b Q)))
3 3an6 1262 . . . 4 (((M Nn P Nn ) (N Nn Q Nn ) (a(1a M a N) b(1b P b Q))) ↔ ((M Nn N Nn a(1a M a N)) (P Nn Q Nn b(1b P b Q))))
4 eeanv 1913 . . . . . 6 (ab((1a M a N) (1b P b Q)) ↔ (a(1a M a N) b(1b P b Q)))
5 simp1l 979 . . . . . . . . . 10 (((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) → M Nn )
6 simp3ll 1026 . . . . . . . . . 10 (((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) → 1a M)
7 ncfinlower 4483 . . . . . . . . . 10 ((M Nn 1a M 1a M) → r Nn (a r a r))
85, 6, 6, 7syl3anc 1182 . . . . . . . . 9 (((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) → r Nn (a r a r))
9 simp1r 980 . . . . . . . . . 10 (((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) → P Nn )
10 simp3rl 1028 . . . . . . . . . 10 (((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) → 1b P)
11 ncfinlower 4483 . . . . . . . . . 10 ((P Nn 1b P 1b P) → s Nn (b s b s))
129, 10, 10, 11syl3anc 1182 . . . . . . . . 9 (((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) → s Nn (b s b s))
13 reeanv 2778 . . . . . . . . . 10 (r Nn s Nn ((a r a r) (b s b s)) ↔ (r Nn (a r a r) s Nn (b s b s)))
14 simpl 443 . . . . . . . . . . . . 13 ((a r a r) → a r)
15 simpl 443 . . . . . . . . . . . . 13 ((b s b s) → b s)
1614, 15anim12i 549 . . . . . . . . . . . 12 (((a r a r) (b s b s)) → (a r b s))
176adantr 451 . . . . . . . . . . . . . . . . 17 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → 1a M)
18 simprll 738 . . . . . . . . . . . . . . . . . 18 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → r Nn )
19 simprrl 740 . . . . . . . . . . . . . . . . . 18 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → a r)
20 tfinpw1 4494 . . . . . . . . . . . . . . . . . 18 ((r Nn a r) → 1a Tfin r)
2118, 19, 20syl2anc 642 . . . . . . . . . . . . . . . . 17 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → 1a Tfin r)
22 elin 3219 . . . . . . . . . . . . . . . . 17 (1a (MTfin r) ↔ (1a M 1a Tfin r))
2317, 21, 22sylanbrc 645 . . . . . . . . . . . . . . . 16 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → 1a (MTfin r))
24 n0i 3555 . . . . . . . . . . . . . . . 16 (1a (MTfin r) → ¬ (MTfin r) = )
2523, 24syl 15 . . . . . . . . . . . . . . 15 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → ¬ (MTfin r) = )
26 simpl1l 1006 . . . . . . . . . . . . . . . 16 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → M Nn )
27 ne0i 3556 . . . . . . . . . . . . . . . . . 18 (a rr)
2819, 27syl 15 . . . . . . . . . . . . . . . . 17 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → r)
29 tfinprop 4489 . . . . . . . . . . . . . . . . . 18 ((r Nn r) → ( Tfin r Nn a r 1a Tfin r))
3029simpld 445 . . . . . . . . . . . . . . . . 17 ((r Nn r) → Tfin r Nn )
3118, 28, 30syl2anc 642 . . . . . . . . . . . . . . . 16 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → Tfin r Nn )
32 nndisjeq 4429 . . . . . . . . . . . . . . . 16 ((M Nn Tfin r Nn ) → ((MTfin r) = M = Tfin r))
3326, 31, 32syl2anc 642 . . . . . . . . . . . . . . 15 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → ((MTfin r) = M = Tfin r))
34 orel1 371 . . . . . . . . . . . . . . 15 (¬ (MTfin r) = → (((MTfin r) = M = Tfin r) → M = Tfin r))
3525, 33, 34sylc 56 . . . . . . . . . . . . . 14 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → M = Tfin r)
3610adantr 451 . . . . . . . . . . . . . . . . 17 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → 1b P)
37 simprlr 739 . . . . . . . . . . . . . . . . . 18 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → s Nn )
38 simprrr 741 . . . . . . . . . . . . . . . . . 18 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → b s)
39 tfinpw1 4494 . . . . . . . . . . . . . . . . . 18 ((s Nn b s) → 1b Tfin s)
4037, 38, 39syl2anc 642 . . . . . . . . . . . . . . . . 17 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → 1b Tfin s)
41 elin 3219 . . . . . . . . . . . . . . . . 17 (1b (PTfin s) ↔ (1b P 1b Tfin s))
4236, 40, 41sylanbrc 645 . . . . . . . . . . . . . . . 16 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → 1b (PTfin s))
43 n0i 3555 . . . . . . . . . . . . . . . 16 (1b (PTfin s) → ¬ (PTfin s) = )
4442, 43syl 15 . . . . . . . . . . . . . . 15 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → ¬ (PTfin s) = )
45 simpl1r 1007 . . . . . . . . . . . . . . . 16 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → P Nn )
46 ne0i 3556 . . . . . . . . . . . . . . . . . 18 (b ss)
4738, 46syl 15 . . . . . . . . . . . . . . . . 17 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → s)
48 tfinprop 4489 . . . . . . . . . . . . . . . . . 18 ((s Nn s) → ( Tfin s Nn a s 1a Tfin s))
4948simpld 445 . . . . . . . . . . . . . . . . 17 ((s Nn s) → Tfin s Nn )
5037, 47, 49syl2anc 642 . . . . . . . . . . . . . . . 16 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → Tfin s Nn )
51 nndisjeq 4429 . . . . . . . . . . . . . . . 16 ((P Nn Tfin s Nn ) → ((PTfin s) = P = Tfin s))
5245, 50, 51syl2anc 642 . . . . . . . . . . . . . . 15 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → ((PTfin s) = P = Tfin s))
53 orel1 371 . . . . . . . . . . . . . . 15 (¬ (PTfin s) = → (((PTfin s) = P = Tfin s) → P = Tfin s))
5444, 52, 53sylc 56 . . . . . . . . . . . . . 14 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → P = Tfin s)
55 tfinltfin 4501 . . . . . . . . . . . . . . . . 17 ((r Nn s Nn ) → (⟪r, s <fin ↔ ⟪ Tfin r, Tfin s <fin ))
5655ad2antrl 708 . . . . . . . . . . . . . . . 16 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → (⟪r, s <fin ↔ ⟪ Tfin r, Tfin s <fin ))
57 opkltfing 4449 . . . . . . . . . . . . . . . . . 18 ((r Nn s Nn ) → (⟪r, s <fin ↔ (r t Nn s = ((r +c t) +c 1c))))
5857ad2antrl 708 . . . . . . . . . . . . . . . . 17 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → (⟪r, s <fin ↔ (r t Nn s = ((r +c t) +c 1c))))
59 simp2rr 1025 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → b s)
60 simp3r 984 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → s = ((r +c t) +c 1c))
6159, 60eleqtrd 2429 . . . . . . . . . . . . . . . . . . . . . . 23 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → b ((r +c t) +c 1c))
62 addcass 4415 . . . . . . . . . . . . . . . . . . . . . . 23 ((r +c t) +c 1c) = (r +c (t +c 1c))
6361, 62syl6eleq 2443 . . . . . . . . . . . . . . . . . . . . . 22 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → b (r +c (t +c 1c)))
64 eladdc 4398 . . . . . . . . . . . . . . . . . . . . . . 23 (b (r +c (t +c 1c)) ↔ g r d (t +c 1c)((gd) = b = (gd)))
65 0nelsuc 4400 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ¬ (t +c 1c)
66 simprlr 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → d (t +c 1c))
67 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (d = → (d (t +c 1c) ↔ (t +c 1c)))
6866, 67syl5ibcom 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → (d = (t +c 1c)))
6965, 68mtoi 169 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → ¬ d = )
70 df-ne 2518 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (d ↔ ¬ d = )
7169, 70sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → d)
72 n0 3559 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (dx x d)
73 ssun2 3427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 d (gd)
74 sseq2 3293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (b = (gd) → (d bd (gd)))
7573, 74mpbiri 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (b = (gd) → d b)
7675sseld 3272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (b = (gd) → (x dx b))
77 disjr 3592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((gd) = x d ¬ x g)
78 rsp 2674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (x d ¬ x g → (x d → ¬ x g))
7977, 78sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((gd) = → (x d → ¬ x g))
8076, 79anim12ii 553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((b = (gd) (gd) = ) → (x d → (x b ¬ x g)))
8180ancoms 439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((gd) = b = (gd)) → (x d → (x b ¬ x g)))
8281ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → (x d → (x b ¬ x g)))
83 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 x V
8483snelpw 4115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ({x} bx b)
8583snelpw 4115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ({x} gx g)
8685notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (¬ {x} g ↔ ¬ x g)
8784, 86anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (({x} b ¬ {x} g) ↔ (x b ¬ x g))
88 ssun1 3426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 g (gd)
89 sseq2 3293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (b = (gd) → (g bg (gd)))
9088, 89mpbiri 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (b = (gd) → g b)
91 sspwb 4118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (g bg b)
9290, 91sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (b = (gd) → g b)
9392adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((gd) = b = (gd)) → g b)
9493ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → g b)
95 eleq2 2414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (g = b → ({x} g ↔ {x} b))
9695biimprcd 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ({x} b → (g = b → {x} g))
9796con3d 125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ({x} b → (¬ {x} g → ¬ g = b))
9897imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (({x} b ¬ {x} g) → ¬ g = b)
9998anim2i 552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((g b ({x} b ¬ {x} g)) → (g b ¬ g = b))
100 dfpss2 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (gb ↔ (g b ¬ g = b))
10199, 100sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((g b ({x} b ¬ {x} g)) → gb)
102 simp2ll 1022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → r Nn )
103102adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → r Nn )
104 simp2rl 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → a r)
105104adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → a r)
106 simprll 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → g r)
107 nnpweq 4523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((r Nn a r g r) → u Nn (a u g u))
108103, 105, 106, 107syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → u Nn (a u g u))
109 simpr2l 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → a u)
110 simp3lr 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) → a N)
1111103ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → a N)
112111ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → a N)
113 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (a (uN) ↔ (a u a N))
114109, 112, 113sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → a (uN))
115 n0i 3555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (a (uN) → ¬ (uN) = )
116114, 115syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → ¬ (uN) = )
117 simpr1 961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → u Nn )
118 simp12l 1068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → N Nn )
119118ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → N Nn )
120 nndisjeq 4429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((u Nn N Nn ) → ((uN) = u = N))
121117, 119, 120syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → ((uN) = u = N))
122 orel1 371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (¬ (uN) = → (((uN) = u = N) → u = N))
123116, 121, 122sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → u = N)
124 simp3rr 1029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) → b Q)
1251243ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → b Q)
126125ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → b Q)
127 simp12r 1069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → Q Nn )
128127ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → Q Nn )
129 elunii 3896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((b Q Q Nn ) → b Nn )
130126, 128, 129syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → b Nn )
131 df-fin 4380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Fin = Nn
132130, 131syl6eleqr 2444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → b Fin )
133 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 b V
134133pwex 4329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 b V
135 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 g V
136135pwex 4329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 g V
137134, 136difex 4107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (b g) V
138 difss 3393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (b g) b
139 ssfin 4470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((b g) V b Fin (b g) b) → (b g) Fin )
140137, 138, 139mp3an13 1268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (b Fin → (b g) Fin )
141132, 140syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → (b g) Fin )
142 elfin 4420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((b g) Finn Nn (b g) n)
143125adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → b Q)
1441433ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → b Q)
145 undif1 3625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((b g) ∪ g) = (bg)
146 uncom 3408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((b g) ∪ g) = (g ∪ (b g))
147145, 146eqtr3i 2375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (bg) = (g ∪ (b g))
148 simp23 990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → gb)
149148pssssd 3366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → g b)
150 ssequn2 3436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (g b ↔ (bg) = b)
151149, 150sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → (bg) = b)
152147, 151syl5eqr 2399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → (g ∪ (b g)) = b)
153 simp22r 1075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → g u)
154 simp3r 984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → (b g) n)
155 disjdif 3622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (g ∩ (b g)) =
156155a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → (g ∩ (b g)) = )
157 eladdci 4399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((g u (b g) n (g ∩ (b g)) = ) → (g ∪ (b g)) (u +c n))
158153, 154, 156, 157syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → (g ∪ (b g)) (u +c n))
159152, 158eqeltrrd 2428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → b (u +c n))
160 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (b (Q ∩ (u +c n)) ↔ (b Q b (u +c n)))
161144, 159, 160sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → b (Q ∩ (u +c n)))
162 n0i 3555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (b (Q ∩ (u +c n)) → ¬ (Q ∩ (u +c n)) = )
163161, 162syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → ¬ (Q ∩ (u +c n)) = )
164127adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → Q Nn )
1651643ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → Q Nn )
166 simp21 988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → u Nn )
167 simp3l 983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → n Nn )
168 nncaddccl 4419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((u Nn n Nn ) → (u +c n) Nn )
169166, 167, 168syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → (u +c n) Nn )
170 nndisjeq 4429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((Q Nn (u +c n) Nn ) → ((Q ∩ (u +c n)) = Q = (u +c n)))
171165, 169, 170syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → ((Q ∩ (u +c n)) = Q = (u +c n)))
172 orel1 371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (¬ (Q ∩ (u +c n)) = → (((Q ∩ (u +c n)) = Q = (u +c n)) → Q = (u +c n)))
173163, 171, 172sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → Q = (u +c n))
174 ne0i 3556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (g uu)
175153, 174syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → u)
176 df-pss 3261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (gb ↔ (g b gb))
177 ssdif0 3609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 (b g ↔ (b g) = )
178 eqss 3287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (g = b ↔ (g b b g))
179178simplbi2 608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 (g b → (b gg = b))
180177, 179syl5bir 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (g b → ((b g) = g = b))
181180necon3d 2554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (g b → (gb → (b g) ≠ ))
182181imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((g b gb) → (b g) ≠ )
183176, 182sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (gb → (b g) ≠ )
184148, 183syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → (b g) ≠ )
185 eleq2 2414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (n = 0c → ((b g) n ↔ (b g) 0c))
186185biimpcd 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((b g) n → (n = 0c → (b g) 0c))
187 el0c 4421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((b g) 0c ↔ (b g) = )
188186, 187syl6ib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((b g) n → (n = 0c → (b g) = ))
189188necon3ad 2552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((b g) n → ((b g) ≠ → ¬ n = 0c))
190154, 184, 189sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → ¬ n = 0c)
191 nnc0suc 4412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (n Nn ↔ (n = 0c m Nn n = (m +c 1c)))
192167, 191sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → (n = 0c m Nn n = (m +c 1c)))
193 orel1 371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 n = 0c → ((n = 0c m Nn n = (m +c 1c)) → m Nn n = (m +c 1c)))
194190, 192, 193sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → m Nn n = (m +c 1c))
195 addceq2 4384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (n = (m +c 1c) → (u +c n) = (u +c (m +c 1c)))
196 addcass 4415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((u +c m) +c 1c) = (u +c (m +c 1c))
197195, 196syl6eqr 2403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (n = (m +c 1c) → (u +c n) = ((u +c m) +c 1c))
198197reximi 2721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (m Nn n = (m +c 1c) → m Nn (u +c n) = ((u +c m) +c 1c))
199194, 198syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → m Nn (u +c n) = ((u +c m) +c 1c))
200 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 u V
201 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 n V
202200, 201addcex 4394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (u +c n) V
203 opkltfing 4449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((u V (u +c n) V) → (⟪u, (u +c n)⟫ <fin ↔ (u m Nn (u +c n) = ((u +c m) +c 1c))))
204200, 202, 203mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (⟪u, (u +c n)⟫ <fin ↔ (u m Nn (u +c n) = ((u +c m) +c 1c)))
205175, 199, 204sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → ⟪u, (u +c n)⟫ <fin )
206 opkeq2 4060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (Q = (u +c n) → ⟪u, Q⟫ = ⟪u, (u +c n)⟫)
207206eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (Q = (u +c n) → (⟪u, Q <fin ↔ ⟪u, (u +c n)⟫ <fin ))
208205, 207syl5ibrcom 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → (Q = (u +c n) → ⟪u, Q <fin ))
209173, 208mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb) (n Nn (b g) n)) → ⟪u, Q <fin )
2102093expa 1151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) (n Nn (b g) n)) → ⟪u, Q <fin )
211210exp32 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → (n Nn → ((b g) n → ⟪u, Q <fin )))
212211rexlimdv 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → (n Nn (b g) n → ⟪u, Q <fin ))
213142, 212syl5bi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → ((b g) Fin → ⟪u, Q <fin ))
214141, 213mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → ⟪u, Q <fin )
215 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (u = N → ⟪u, Q⟫ = ⟪N, Q⟫)
216215eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (u = N → (⟪u, Q <fin ↔ ⟪N, Q <fin ))
217214, 216syl5ibcom 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → (u = N → ⟪N, Q <fin ))
218123, 217mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) (u Nn (a u g u) gb)) → ⟪N, Q <fin )
2192183exp2 1169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → (u Nn → ((a u g u) → (gb → ⟪N, Q <fin ))))
220219rexlimdv 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → (u Nn (a u g u) → (gb → ⟪N, Q <fin )))
221108, 220mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → (gb → ⟪N, Q <fin ))
222101, 221syl5 28 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → ((g b ({x} b ¬ {x} g)) → ⟪N, Q <fin ))
22394, 222mpand 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → (({x} b ¬ {x} g) → ⟪N, Q <fin ))
22487, 223syl5bir 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → ((x b ¬ x g) → ⟪N, Q <fin ))
22582, 224syld 40 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → (x d → ⟪N, Q <fin ))
226225exlimdv 1636 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → (x x d → ⟪N, Q <fin ))
22772, 226syl5bi 208 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → (d → ⟪N, Q <fin ))
22871, 227mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) ((g r d (t +c 1c)) ((gd) = b = (gd)))) → ⟪N, Q <fin )
229228exp32 588 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → ((g r d (t +c 1c)) → (((gd) = b = (gd)) → ⟪N, Q <fin )))
230229rexlimdvv 2744 . . . . . . . . . . . . . . . . . . . . . . 23 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → (g r d (t +c 1c)((gd) = b = (gd)) → ⟪N, Q <fin ))
23164, 230syl5bi 208 . . . . . . . . . . . . . . . . . . . . . 22 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → (b (r +c (t +c 1c)) → ⟪N, Q <fin ))
23263, 231mpd 14 . . . . . . . . . . . . . . . . . . . . 21 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s)) (t Nn s = ((r +c t) +c 1c))) → ⟪N, Q <fin )
2332323expa 1151 . . . . . . . . . . . . . . . . . . . 20 (((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) (t Nn s = ((r +c t) +c 1c))) → ⟪N, Q <fin )
234233exp32 588 . . . . . . . . . . . . . . . . . . 19 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → (t Nn → (s = ((r +c t) +c 1c) → ⟪N, Q <fin )))
235234rexlimdv 2737 . . . . . . . . . . . . . . . . . 18 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → (t Nn s = ((r +c t) +c 1c) → ⟪N, Q <fin ))
236235adantld 453 . . . . . . . . . . . . . . . . 17 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → ((r t Nn s = ((r +c t) +c 1c)) → ⟪N, Q <fin ))
23758, 236sylbid 206 . . . . . . . . . . . . . . . 16 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → (⟪r, s <fin → ⟪N, Q <fin ))
23856, 237sylbird 226 . . . . . . . . . . . . . . 15 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → (⟪ Tfin r, Tfin s <fin → ⟪N, Q <fin ))
239 opkeq12 4061 . . . . . . . . . . . . . . . . 17 ((M = Tfin r P = Tfin s) → ⟪M, P⟫ = ⟪ Tfin r, Tfin s⟫)
240239eleq1d 2419 . . . . . . . . . . . . . . . 16 ((M = Tfin r P = Tfin s) → (⟪M, P <fin ↔ ⟪ Tfin r, Tfin s <fin ))
241240imbi1d 308 . . . . . . . . . . . . . . 15 ((M = Tfin r P = Tfin s) → ((⟪M, P <fin → ⟪N, Q <fin ) ↔ (⟪ Tfin r, Tfin s <fin → ⟪N, Q <fin )))
242238, 241syl5ibrcom 213 . . . . . . . . . . . . . 14 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → ((M = Tfin r P = Tfin s) → (⟪M, P <fin → ⟪N, Q <fin )))
24335, 54, 242mp2and 660 . . . . . . . . . . . . 13 ((((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) ((r Nn s Nn ) (a r b s))) → (⟪M, P <fin → ⟪N, Q <fin ))
244243exp32 588 . . . . . . . . . . . 12 (((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) → ((r Nn s Nn ) → ((a r b s) → (⟪M, P <fin → ⟪N, Q <fin ))))
24516, 244syl7 63 . . . . . . . . . . 11 (((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) → ((r Nn s Nn ) → (((a r a r) (b s b s)) → (⟪M, P <fin → ⟪N, Q <fin ))))
246245rexlimdvv 2744 . . . . . . . . . 10 (((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) → (r Nn s Nn ((a r a r) (b s b s)) → (⟪M, P <fin → ⟪N, Q <fin )))
24713, 246syl5bir 209 . . . . . . . . 9 (((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) → ((r Nn (a r a r) s Nn (b s b s)) → (⟪M, P <fin → ⟪N, Q <fin )))
2488, 12, 247mp2and 660 . . . . . . . 8 (((M Nn P Nn ) (N Nn Q Nn ) ((1a M a N) (1b P b Q))) → (⟪M, P <fin → ⟪N, Q <fin ))
2492483expia 1153 . . . . . . 7 (((M Nn P Nn ) (N Nn Q Nn )) → (((1a M a N) (1b P b Q)) → (⟪M, P <fin → ⟪N, Q <fin )))
250249exlimdvv 1637 . . . . . 6 (((M Nn P Nn ) (N Nn Q Nn )) → (ab((1a M a N) (1b P b Q)) → (⟪M, P <fin → ⟪N, Q <fin )))
2514, 250syl5bir 209 . . . . 5 (((M Nn P Nn ) (N Nn Q Nn )) → ((a(1a M a N) b(1b P b Q)) → (⟪M, P <fin → ⟪N, Q <fin )))
2522513impia 1148 . . . 4 (((M Nn P Nn ) (N Nn Q Nn ) (a(1a M a N) b(1b P b Q))) → (⟪M, P <fin → ⟪N, Q <fin ))
2533, 252sylbir 204 . . 3 (((M Nn N Nn a(1a M a N)) (P Nn Q Nn b(1b P b Q))) → (⟪M, P <fin → ⟪N, Q <fin ))
2541, 2, 253syl2anb 465 . 2 (( Sfin (M, N) Sfin (P, Q)) → (⟪M, P <fin → ⟪N, Q <fin ))
255254imp 418 1 ((( Sfin (M, N) Sfin (P, Q)) M, P <fin ) → ⟪N, Q <fin )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wo 357   wa 358   w3a 934  wex 1541   = wceq 1642   wcel 1710  wne 2516  wral 2614  wrex 2615  Vcvv 2859   cdif 3206  cun 3207  cin 3208   wss 3257  wpss 3258  c0 3550  cpw 3722  {csn 3737  cuni 3891  copk 4057  1cc1c 4134  1cpw1 4135   Nn cnnc 4373  0cc0c 4374   +c cplc 4375   Fin cfin 4376   <fin cltfin 4433   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-3or 935  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-pss 3261  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-fin 4380  df-lefin 4440  df-ltfin 4441  df-tfin 4443  df-sfin 4446
This theorem is referenced by:  sfin111  4536  vfinspsslem1  4550
  Copyright terms: Public domain W3C validator