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

Theorem ssfin 4470
Description: A subset of a finite set is itself finite. Theorem X.1.21 of [Rosser] p. 527. (Contributed by SF, 19-Jan-2015.)
Assertion
Ref Expression
ssfin ((A V B Fin A B) → A Fin )

Proof of Theorem ssfin
Dummy variables a b c d k m n x t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 3292 . . . . 5 (a = A → (a BA B))
2 eleq1 2413 . . . . 5 (a = A → (a FinA Fin ))
31, 2imbi12d 311 . . . 4 (a = A → ((a Ba Fin ) ↔ (A BA Fin )))
43imbi2d 307 . . 3 (a = A → ((B Fin → (a Ba Fin )) ↔ (B Fin → (A BA Fin ))))
5 sseq2 3293 . . . . 5 (b = B → (a ba B))
65imbi1d 308 . . . 4 (b = B → ((a ba Fin ) ↔ (a Ba Fin )))
7 elfin 4420 . . . . 5 (b Finn Nn b n)
8 vex 2862 . . . . . . . . . . . . 13 m V
98elcompl 3225 . . . . . . . . . . . 12 (m ∼ (( Sk ∩ (1( SkkFin ) ×k V)) “k 1c) ↔ ¬ m (( Sk ∩ (1( SkkFin ) ×k V)) “k 1c))
10 alcom 1737 . . . . . . . . . . . . 13 (ab((b m a b) → a Fin ) ↔ ba((b m a b) → a Fin ))
11 impexp 433 . . . . . . . . . . . . . . . 16 (((b m a b) → a Fin ) ↔ (b m → (a ba Fin )))
1211albii 1566 . . . . . . . . . . . . . . 15 (a((b m a b) → a Fin ) ↔ a(b m → (a ba Fin )))
13 19.21v 1890 . . . . . . . . . . . . . . 15 (a(b m → (a ba Fin )) ↔ (b ma(a ba Fin )))
1412, 13bitri 240 . . . . . . . . . . . . . 14 (a((b m a b) → a Fin ) ↔ (b ma(a ba Fin )))
1514albii 1566 . . . . . . . . . . . . 13 (ba((b m a b) → a Fin ) ↔ b(b ma(a ba Fin )))
168elimak 4259 . . . . . . . . . . . . . . 15 (m (( Sk ∩ (1( SkkFin ) ×k V)) “k 1c) ↔ t 1ct, m ( Sk ∩ (1( SkkFin ) ×k V)))
17 df-rex 2620 . . . . . . . . . . . . . . . 16 (t 1ct, m ( Sk ∩ (1( SkkFin ) ×k V)) ↔ t(t 1c t, m ( Sk ∩ (1( SkkFin ) ×k V))))
18 el1c 4139 . . . . . . . . . . . . . . . . . . . 20 (t 1cb t = {b})
1918anbi1i 676 . . . . . . . . . . . . . . . . . . 19 ((t 1c t, m ( Sk ∩ (1( SkkFin ) ×k V))) ↔ (b t = {b} t, m ( Sk ∩ (1( SkkFin ) ×k V))))
20 19.41v 1901 . . . . . . . . . . . . . . . . . . 19 (b(t = {b} t, m ( Sk ∩ (1( SkkFin ) ×k V))) ↔ (b t = {b} t, m ( Sk ∩ (1( SkkFin ) ×k V))))
2119, 20bitr4i 243 . . . . . . . . . . . . . . . . . 18 ((t 1c t, m ( Sk ∩ (1( SkkFin ) ×k V))) ↔ b(t = {b} t, m ( Sk ∩ (1( SkkFin ) ×k V))))
2221exbii 1582 . . . . . . . . . . . . . . . . 17 (t(t 1c t, m ( Sk ∩ (1( SkkFin ) ×k V))) ↔ tb(t = {b} t, m ( Sk ∩ (1( SkkFin ) ×k V))))
23 excom 1741 . . . . . . . . . . . . . . . . 17 (bt(t = {b} t, m ( Sk ∩ (1( SkkFin ) ×k V))) ↔ tb(t = {b} t, m ( Sk ∩ (1( SkkFin ) ×k V))))
2422, 23bitr4i 243 . . . . . . . . . . . . . . . 16 (t(t 1c t, m ( Sk ∩ (1( SkkFin ) ×k V))) ↔ bt(t = {b} t, m ( Sk ∩ (1( SkkFin ) ×k V))))
25 snex 4111 . . . . . . . . . . . . . . . . . . 19 {b} V
26 opkeq1 4059 . . . . . . . . . . . . . . . . . . . 20 (t = {b} → ⟪t, m⟫ = ⟪{b}, m⟫)
2726eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 (t = {b} → (⟪t, m ( Sk ∩ (1( SkkFin ) ×k V)) ↔ ⟪{b}, m ( Sk ∩ (1( SkkFin ) ×k V))))
2825, 27ceqsexv 2894 . . . . . . . . . . . . . . . . . 18 (t(t = {b} t, m ( Sk ∩ (1( SkkFin ) ×k V))) ↔ ⟪{b}, m ( Sk ∩ (1( SkkFin ) ×k V)))
29 elin 3219 . . . . . . . . . . . . . . . . . 18 (⟪{b}, m ( Sk ∩ (1( SkkFin ) ×k V)) ↔ (⟪{b}, m Sk ⟪{b}, m (1( SkkFin ) ×k V)))
30 vex 2862 . . . . . . . . . . . . . . . . . . . 20 b V
3130, 8elssetk 4270 . . . . . . . . . . . . . . . . . . 19 (⟪{b}, m Skb m)
3225, 8opkelxpk 4248 . . . . . . . . . . . . . . . . . . . . 21 (⟪{b}, m (1( SkkFin ) ×k V) ↔ ({b} 1( SkkFin ) m V))
338, 32mpbiran2 885 . . . . . . . . . . . . . . . . . . . 20 (⟪{b}, m (1( SkkFin ) ×k V) ↔ {b} 1( SkkFin ))
34 snelpw1 4146 . . . . . . . . . . . . . . . . . . . 20 ({b} 1( SkkFin ) ↔ b ( SkkFin ))
3530elimak 4259 . . . . . . . . . . . . . . . . . . . . 21 (b ( SkkFin ) ↔ a Fina, b Sk )
36 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . 22 (a Fina, b Ska(a Fin a, b Sk ))
37 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a Fin a, b Sk ) ↔ (⟪a, b Sk a Fin ))
38 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . 26 a V
39 opkelssetkg 4268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a V b V) → (⟪a, b Ska b))
4038, 30, 39mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪a, b Ska b)
4138elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a Fin ↔ ¬ a Fin )
4240, 41anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟪a, b Sk a Fin ) ↔ (a b ¬ a Fin ))
4337, 42bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23 ((a Fin a, b Sk ) ↔ (a b ¬ a Fin ))
4443exbii 1582 . . . . . . . . . . . . . . . . . . . . . 22 (a(a Fin a, b Sk ) ↔ a(a b ¬ a Fin ))
4536, 44bitri 240 . . . . . . . . . . . . . . . . . . . . 21 (a Fina, b Ska(a b ¬ a Fin ))
46 exanali 1585 . . . . . . . . . . . . . . . . . . . . 21 (a(a b ¬ a Fin ) ↔ ¬ a(a ba Fin ))
4735, 45, 463bitri 262 . . . . . . . . . . . . . . . . . . . 20 (b ( SkkFin ) ↔ ¬ a(a ba Fin ))
4833, 34, 473bitri 262 . . . . . . . . . . . . . . . . . . 19 (⟪{b}, m (1( SkkFin ) ×k V) ↔ ¬ a(a ba Fin ))
4931, 48anbi12i 678 . . . . . . . . . . . . . . . . . 18 ((⟪{b}, m Sk ⟪{b}, m (1( SkkFin ) ×k V)) ↔ (b m ¬ a(a ba Fin )))
5028, 29, 493bitri 262 . . . . . . . . . . . . . . . . 17 (t(t = {b} t, m ( Sk ∩ (1( SkkFin ) ×k V))) ↔ (b m ¬ a(a ba Fin )))
5150exbii 1582 . . . . . . . . . . . . . . . 16 (bt(t = {b} t, m ( Sk ∩ (1( SkkFin ) ×k V))) ↔ b(b m ¬ a(a ba Fin )))
5217, 24, 513bitri 262 . . . . . . . . . . . . . . 15 (t 1ct, m ( Sk ∩ (1( SkkFin ) ×k V)) ↔ b(b m ¬ a(a ba Fin )))
53 exanali 1585 . . . . . . . . . . . . . . 15 (b(b m ¬ a(a ba Fin )) ↔ ¬ b(b ma(a ba Fin )))
5416, 52, 533bitri 262 . . . . . . . . . . . . . 14 (m (( Sk ∩ (1( SkkFin ) ×k V)) “k 1c) ↔ ¬ b(b ma(a ba Fin )))
5554con2bii 322 . . . . . . . . . . . . 13 (b(b ma(a ba Fin )) ↔ ¬ m (( Sk ∩ (1( SkkFin ) ×k V)) “k 1c))
5610, 15, 553bitri 262 . . . . . . . . . . . 12 (ab((b m a b) → a Fin ) ↔ ¬ m (( Sk ∩ (1( SkkFin ) ×k V)) “k 1c))
579, 56bitr4i 243 . . . . . . . . . . 11 (m ∼ (( Sk ∩ (1( SkkFin ) ×k V)) “k 1c) ↔ ab((b m a b) → a Fin ))
5857abbi2i 2464 . . . . . . . . . 10 ∼ (( Sk ∩ (1( SkkFin ) ×k V)) “k 1c) = {m ab((b m a b) → a Fin )}
59 ssetkex 4294 . . . . . . . . . . . . 13 Sk V
60 finex 4397 . . . . . . . . . . . . . . . . 17 Fin V
6160complex 4104 . . . . . . . . . . . . . . . 16 Fin V
6259, 61imakex 4300 . . . . . . . . . . . . . . 15 ( SkkFin ) V
6362pw1ex 4303 . . . . . . . . . . . . . 14 1( SkkFin ) V
64 vvex 4109 . . . . . . . . . . . . . 14 V V
6563, 64xpkex 4289 . . . . . . . . . . . . 13 (1( SkkFin ) ×k V) V
6659, 65inex 4105 . . . . . . . . . . . 12 ( Sk ∩ (1( SkkFin ) ×k V)) V
67 1cex 4142 . . . . . . . . . . . 12 1c V
6866, 67imakex 4300 . . . . . . . . . . 11 (( Sk ∩ (1( SkkFin ) ×k V)) “k 1c) V
6968complex 4104 . . . . . . . . . 10 ∼ (( Sk ∩ (1( SkkFin ) ×k V)) “k 1c) V
7058, 69eqeltrri 2424 . . . . . . . . 9 {m ab((b m a b) → a Fin )} V
71 eleq2 2414 . . . . . . . . . . . . 13 (m = 0c → (b mb 0c))
72 df-0c 4377 . . . . . . . . . . . . . . 15 0c = {}
7372eleq2i 2417 . . . . . . . . . . . . . 14 (b 0cb {})
7430elsnc 3756 . . . . . . . . . . . . . 14 (b {} ↔ b = )
7573, 74bitri 240 . . . . . . . . . . . . 13 (b 0cb = )
7671, 75syl6bb 252 . . . . . . . . . . . 12 (m = 0c → (b mb = ))
7776anbi1d 685 . . . . . . . . . . 11 (m = 0c → ((b m a b) ↔ (b = a b)))
7877imbi1d 308 . . . . . . . . . 10 (m = 0c → (((b m a b) → a Fin ) ↔ ((b = a b) → a Fin )))
79782albidv 1627 . . . . . . . . 9 (m = 0c → (ab((b m a b) → a Fin ) ↔ ab((b = a b) → a Fin )))
80 elequ2 1715 . . . . . . . . . . . . 13 (m = k → (b mb k))
8180anbi1d 685 . . . . . . . . . . . 12 (m = k → ((b m a b) ↔ (b k a b)))
8281imbi1d 308 . . . . . . . . . . 11 (m = k → (((b m a b) → a Fin ) ↔ ((b k a b) → a Fin )))
83822albidv 1627 . . . . . . . . . 10 (m = k → (ab((b m a b) → a Fin ) ↔ ab((b k a b) → a Fin )))
84 eleq1 2413 . . . . . . . . . . . . . 14 (b = d → (b kd k))
8584adantl 452 . . . . . . . . . . . . 13 ((a = c b = d) → (b kd k))
86 sseq12 3294 . . . . . . . . . . . . 13 ((a = c b = d) → (a bc d))
8785, 86anbi12d 691 . . . . . . . . . . . 12 ((a = c b = d) → ((b k a b) ↔ (d k c d)))
88 eleq1 2413 . . . . . . . . . . . . 13 (a = c → (a Finc Fin ))
8988adantr 451 . . . . . . . . . . . 12 ((a = c b = d) → (a Finc Fin ))
9087, 89imbi12d 311 . . . . . . . . . . 11 ((a = c b = d) → (((b k a b) → a Fin ) ↔ ((d k c d) → c Fin )))
9190cbval2v 2006 . . . . . . . . . 10 (ab((b k a b) → a Fin ) ↔ cd((d k c d) → c Fin ))
9283, 91syl6bb 252 . . . . . . . . 9 (m = k → (ab((b m a b) → a Fin ) ↔ cd((d k c d) → c Fin )))
93 eleq2 2414 . . . . . . . . . . . 12 (m = (k +c 1c) → (b mb (k +c 1c)))
9493anbi1d 685 . . . . . . . . . . 11 (m = (k +c 1c) → ((b m a b) ↔ (b (k +c 1c) a b)))
9594imbi1d 308 . . . . . . . . . 10 (m = (k +c 1c) → (((b m a b) → a Fin ) ↔ ((b (k +c 1c) a b) → a Fin )))
96952albidv 1627 . . . . . . . . 9 (m = (k +c 1c) → (ab((b m a b) → a Fin ) ↔ ab((b (k +c 1c) a b) → a Fin )))
97 elequ2 1715 . . . . . . . . . . . 12 (m = n → (b mb n))
9897anbi1d 685 . . . . . . . . . . 11 (m = n → ((b m a b) ↔ (b n a b)))
9998imbi1d 308 . . . . . . . . . 10 (m = n → (((b m a b) → a Fin ) ↔ ((b n a b) → a Fin )))
100992albidv 1627 . . . . . . . . 9 (m = n → (ab((b m a b) → a Fin ) ↔ ab((b n a b) → a Fin )))
101 sseq2 3293 . . . . . . . . . . . . 13 (b = → (a ba ))
102101biimpa 470 . . . . . . . . . . . 12 ((b = a b) → a )
103 ss0b 3580 . . . . . . . . . . . 12 (a a = )
104102, 103sylib 188 . . . . . . . . . . 11 ((b = a b) → a = )
105 0fin 4423 . . . . . . . . . . 11 Fin
106104, 105syl6eqel 2441 . . . . . . . . . 10 ((b = a b) → a Fin )
107106gen2 1547 . . . . . . . . 9 ab((b = a b) → a Fin )
108 sspss 3368 . . . . . . . . . . . . . . 15 (a b ↔ (ab a = b))
109 dfpss4 3888 . . . . . . . . . . . . . . . 16 (ab ↔ (a b x b ¬ x a))
110109orbi1i 506 . . . . . . . . . . . . . . 15 ((ab a = b) ↔ ((a b x b ¬ x a) a = b))
111108, 110bitri 240 . . . . . . . . . . . . . 14 (a b ↔ ((a b x b ¬ x a) a = b))
112 simp1 955 . . . . . . . . . . . . . . . . . . . . . . . 24 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → k Nn )
113 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 x V
114113snid 3760 . . . . . . . . . . . . . . . . . . . . . . . . . 26 x {x}
115 eldif 3221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (x (b {x}) ↔ (x b ¬ x {x}))
116115simprbi 450 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (x (b {x}) → ¬ x {x})
117114, 116mt2 170 . . . . . . . . . . . . . . . . . . . . . . . . 25 ¬ x (b {x})
118117a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → ¬ x (b {x}))
119 undif1 3625 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((b {x}) ∪ {x}) = (b ∪ {x})
120 snssi 3852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (x b → {x} b)
121 ssequn2 3436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({x} b ↔ (b ∪ {x}) = b)
122120, 121sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (x b → (b ∪ {x}) = b)
123122adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((x b ¬ x a) → (b ∪ {x}) = b)
1241233ad2ant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → (b ∪ {x}) = b)
125119, 124syl5eq 2397 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → ((b {x}) ∪ {x}) = b)
126 simp3r 984 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → b (k +c 1c))
127125, 126eqeltrd 2427 . . . . . . . . . . . . . . . . . . . . . . . 24 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → ((b {x}) ∪ {x}) (k +c 1c))
128 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {x} V
12930, 128difex 4107 . . . . . . . . . . . . . . . . . . . . . . . . 25 (b {x}) V
130129, 113nnsucelr 4428 . . . . . . . . . . . . . . . . . . . . . . . 24 ((k Nn x (b {x}) ((b {x}) ∪ {x}) (k +c 1c))) → (b {x}) k)
131112, 118, 127, 130syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . . 23 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → (b {x}) k)
132 inass 3465 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ab) ∩ ∼ {x}) = (a ∩ (b ∩ ∼ {x}))
133 df-dif 3215 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ab) {x}) = ((ab) ∩ ∼ {x})
134 df-dif 3215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (b {x}) = (b ∩ ∼ {x})
135134ineq2i 3454 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a ∩ (b {x})) = (a ∩ (b ∩ ∼ {x}))
136132, 133, 1353eqtr4ri 2384 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a ∩ (b {x})) = ((ab) {x})
137 df-ss 3259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (a b ↔ (ab) = a)
138137biimpi 186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (a b → (ab) = a)
139138adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a b b (k +c 1c)) → (ab) = a)
1401393ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → (ab) = a)
141140difeq1d 3384 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → ((ab) {x}) = (a {x}))
142 difsn 3845 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 x a → (a {x}) = a)
143142adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((x b ¬ x a) → (a {x}) = a)
1441433ad2ant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → (a {x}) = a)
145141, 144eqtrd 2385 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → ((ab) {x}) = a)
146136, 145syl5eq 2397 . . . . . . . . . . . . . . . . . . . . . . . 24 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → (a ∩ (b {x})) = a)
147 df-ss 3259 . . . . . . . . . . . . . . . . . . . . . . . 24 (a (b {x}) ↔ (a ∩ (b {x})) = a)
148146, 147sylibr 203 . . . . . . . . . . . . . . . . . . . . . . 23 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → a (b {x}))
149131, 148jca 518 . . . . . . . . . . . . . . . . . . . . . 22 ((k Nn (x b ¬ x a) (a b b (k +c 1c))) → ((b {x}) k a (b {x})))
1501493adant1r 1175 . . . . . . . . . . . . . . . . . . . . 21 (((k Nn cd((d k c d) → c Fin )) (x b ¬ x a) (a b b (k +c 1c))) → ((b {x}) k a (b {x})))
151 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (d = (b {x}) → (d k ↔ (b {x}) k))
152151adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((c = a d = (b {x})) → (d k ↔ (b {x}) k))
153 sseq12 3294 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((c = a d = (b {x})) → (c da (b {x})))
154152, 153anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((c = a d = (b {x})) → ((d k c d) ↔ ((b {x}) k a (b {x}))))
155 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (c = a → (c Fina Fin ))
156155adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((c = a d = (b {x})) → (c Fina Fin ))
157154, 156imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((c = a d = (b {x})) → (((d k c d) → c Fin ) ↔ (((b {x}) k a (b {x})) → a Fin )))
158157spc2gv 2942 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a V (b {x}) V) → (cd((d k c d) → c Fin ) → (((b {x}) k a (b {x})) → a Fin )))
15938, 129, 158mp2an 653 . . . . . . . . . . . . . . . . . . . . . . 23 (cd((d k c d) → c Fin ) → (((b {x}) k a (b {x})) → a Fin ))
160159adantl 452 . . . . . . . . . . . . . . . . . . . . . 22 ((k Nn cd((d k c d) → c Fin )) → (((b {x}) k a (b {x})) → a Fin ))
1611603ad2ant1 976 . . . . . . . . . . . . . . . . . . . . 21 (((k Nn cd((d k c d) → c Fin )) (x b ¬ x a) (a b b (k +c 1c))) → (((b {x}) k a (b {x})) → a Fin ))
162150, 161mpd 14 . . . . . . . . . . . . . . . . . . . 20 (((k Nn cd((d k c d) → c Fin )) (x b ¬ x a) (a b b (k +c 1c))) → a Fin )
1631623exp 1150 . . . . . . . . . . . . . . . . . . 19 ((k Nn cd((d k c d) → c Fin )) → ((x b ¬ x a) → ((a b b (k +c 1c)) → a Fin )))
164163exp5c 599 . . . . . . . . . . . . . . . . . 18 ((k Nn cd((d k c d) → c Fin )) → (x b → (¬ x a → (a b → (b (k +c 1c) → a Fin )))))
165164rexlimdv 2737 . . . . . . . . . . . . . . . . 17 ((k Nn cd((d k c d) → c Fin )) → (x b ¬ x a → (a b → (b (k +c 1c) → a Fin ))))
166165com23 72 . . . . . . . . . . . . . . . 16 ((k Nn cd((d k c d) → c Fin )) → (a b → (x b ¬ x a → (b (k +c 1c) → a Fin ))))
167166imp3a 420 . . . . . . . . . . . . . . 15 ((k Nn cd((d k c d) → c Fin )) → ((a b x b ¬ x a) → (b (k +c 1c) → a Fin )))
168 peano2 4403 . . . . . . . . . . . . . . . . . 18 (k Nn → (k +c 1c) Nn )
169 eleq2 2414 . . . . . . . . . . . . . . . . . . . . 21 (x = (k +c 1c) → (b xb (k +c 1c)))
170169rspcev 2955 . . . . . . . . . . . . . . . . . . . 20 (((k +c 1c) Nn b (k +c 1c)) → x Nn b x)
171 elfin 4420 . . . . . . . . . . . . . . . . . . . 20 (b Finx Nn b x)
172170, 171sylibr 203 . . . . . . . . . . . . . . . . . . 19 (((k +c 1c) Nn b (k +c 1c)) → b Fin )
173172ex 423 . . . . . . . . . . . . . . . . . 18 ((k +c 1c) Nn → (b (k +c 1c) → b Fin ))
174168, 173syl 15 . . . . . . . . . . . . . . . . 17 (k Nn → (b (k +c 1c) → b Fin ))
175 eleq1 2413 . . . . . . . . . . . . . . . . . 18 (a = b → (a Finb Fin ))
176175biimprd 214 . . . . . . . . . . . . . . . . 17 (a = b → (b Fina Fin ))
177174, 176syl9 66 . . . . . . . . . . . . . . . 16 (k Nn → (a = b → (b (k +c 1c) → a Fin )))
178177adantr 451 . . . . . . . . . . . . . . 15 ((k Nn cd((d k c d) → c Fin )) → (a = b → (b (k +c 1c) → a Fin )))
179167, 178jaod 369 . . . . . . . . . . . . . 14 ((k Nn cd((d k c d) → c Fin )) → (((a b x b ¬ x a) a = b) → (b (k +c 1c) → a Fin )))
180111, 179syl5bi 208 . . . . . . . . . . . . 13 ((k Nn cd((d k c d) → c Fin )) → (a b → (b (k +c 1c) → a Fin )))
181180com23 72 . . . . . . . . . . . 12 ((k Nn cd((d k c d) → c Fin )) → (b (k +c 1c) → (a ba Fin )))
182181imp3a 420 . . . . . . . . . . 11 ((k Nn cd((d k c d) → c Fin )) → ((b (k +c 1c) a b) → a Fin ))
183182alrimivv 1632 . . . . . . . . . 10 ((k Nn cd((d k c d) → c Fin )) → ab((b (k +c 1c) a b) → a Fin ))
184183ex 423 . . . . . . . . 9 (k Nn → (cd((d k c d) → c Fin ) → ab((b (k +c 1c) a b) → a Fin )))
18570, 79, 92, 96, 100, 107, 184finds 4411 . . . . . . . 8 (n Nnab((b n a b) → a Fin ))
18618519.21bbi 1865 . . . . . . 7 (n Nn → ((b n a b) → a Fin ))
187186exp3a 425 . . . . . 6 (n Nn → (b n → (a ba Fin )))
188187rexlimiv 2732 . . . . 5 (n Nn b n → (a ba Fin ))
1897, 188sylbi 187 . . . 4 (b Fin → (a ba Fin ))
1906, 189vtoclga 2920 . . 3 (B Fin → (a Ba Fin ))
1914, 190vtoclg 2914 . 2 (A V → (B Fin → (A BA Fin )))
1921913imp 1145 1 ((A V B Fin A B) → A Fin )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wo 357   wa 358   w3a 934  wal 1540  wex 1541   = wceq 1642   wcel 1710  {cab 2339  wrex 2615  Vcvv 2859  ccompl 3205   cdif 3206  cun 3207  cin 3208   wss 3257  wpss 3258  c0 3550  {csn 3737  copk 4057  1cc1c 4134  1cpw1 4135   ×k cxpk 4174  k cimak 4179   Sk cssetk 4183   Nn cnnc 4373  0cc0c 4374   +c cplc 4375   Fin cfin 4376
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-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-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  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-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380
This theorem is referenced by:  vfinnc  4471  sfinltfin  4535
  Copyright terms: Public domain W3C validator