Theorem vfinspclt 4553

Description: If the universe is finite, then Sp_fin is closed under T-raising. Theorem X.1.60 of [Rosser] p. 536. (Contributed by SF, 30-Jan-2015.)

Assertion

Ref	Expression
vfinspclt	|- ((_V e. Fin /\ X e. Spfin ) -> Tfin X e. Spfin )

Proof of Theorem vfinspclt

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tncveqnc1fin 4545	. . . . . 6 |- (_V e. Fin -> Tfin Ncfin _V = Ncfin 1c)
2		1cspfin 4544	. . . . . 6 |- (_V e. Fin -> Ncfin 1c e. Spfin )
3	1, 2	eqeltrd 2427	. . . . 5 |- (_V e. Fin -> Tfin Ncfin _V e. Spfin )
4		ncfinex 4473	. . . . . 6 |- Ncfin _V e. _V
5		tfineq 4489	. . . . . . 7 |- (x = Ncfin _V -> Tfin x = Tfin Ncfin _V)
6	5	eleq1d 2419	. . . . . 6 |- (x = Ncfin _V -> ( Tfin x e. Spfin <-> Tfin Ncfin _V e. Spfin ))
7	4, 6	elab 2986	. . . . 5 |- ( Ncfin _V e. {x | Tfin x e. Spfin } <-> Tfin Ncfin _V e. Spfin )
8	3, 7	sylibr 203	. . . 4 |- (_V e. Fin -> Ncfin _V e. {x | Tfin x e. Spfin })
9		simprl 732	. . . . . . . . 9 |- (((_V e. Fin /\ y e. Spfin ) /\ ( Tfin y e. Spfin /\ Sfin (z, y))) -> Tfin y e. Spfin )
10		sfintfin 4533	. . . . . . . . . 10 |- ( Sfin (z, y) -> Sfin ( Tfin z, Tfin y))
11	10	ad2antll 709	. . . . . . . . 9 |- (((_V e. Fin /\ y e. Spfin ) /\ ( Tfin y e. Spfin /\ Sfin (z, y))) -> Sfin ( Tfin z, Tfin y))
12		spfinsfincl 4540	. . . . . . . . 9 |- (( Tfin y e. Spfin /\ Sfin ( Tfin z, Tfin y)) -> Tfin z e. Spfin )
13	9, 11, 12	syl2anc 642	. . . . . . . 8 |- (((_V e. Fin /\ y e. Spfin ) /\ ( Tfin y e. Spfin /\ Sfin (z, y))) -> Tfin z e. Spfin )
14	13	ex 423	. . . . . . 7 |- ((_V e. Fin /\ y e. Spfin ) -> (( Tfin y e. Spfin /\ Sfin (z, y)) -> Tfin z e. Spfin ))
15		vex 2863	. . . . . . . . 9 |- y e. _V
16		tfineq 4489	. . . . . . . . . 10 |- (x = y -> Tfin x = Tfin y)
17	16	eleq1d 2419	. . . . . . . . 9 |- (x = y -> ( Tfin x e. Spfin <-> Tfin y e. Spfin ))
18	15, 17	elab 2986	. . . . . . . 8 |- (y e. {x | Tfin x e. Spfin } <-> Tfin y e. Spfin )
19	18	anbi1i 676	. . . . . . 7 |- ((y e. {x | Tfin x e. Spfin } /\ Sfin (z, y)) <-> ( Tfin y e. Spfin /\ Sfin (z, y)))
20		vex 2863	. . . . . . . 8 |- z e. _V
21		tfineq 4489	. . . . . . . . 9 |- (x = z -> Tfin x = Tfin z)
22	21	eleq1d 2419	. . . . . . . 8 |- (x = z -> ( Tfin x e. Spfin <-> Tfin z e. Spfin ))
23	20, 22	elab 2986	. . . . . . 7 |- (z e. {x | Tfin x e. Spfin } <-> Tfin z e. Spfin )
24	14, 19, 23	3imtr4g 261	. . . . . 6 |- ((_V e. Fin /\ y e. Spfin ) -> ((y e. {x | Tfin x e. Spfin } /\ Sfin (z, y)) -> z e. {x | Tfin x e. Spfin }))
25	24	alrimiv 1631	. . . . 5 |- ((_V e. Fin /\ y e. Spfin ) -> A.z((y e. {x | Tfin x e. Spfin } /\ Sfin (z, y)) -> z e. {x | Tfin x e. Spfin }))
26	25	ralrimiva 2698	. . . 4 |- (_V e. Fin -> A.y e. Spfin A.z((y e. {x | Tfin x e. Spfin } /\ Sfin (z, y)) -> z e. {x | Tfin x e. Spfin }))
27		snex 4112	. . . . . . . . . 10 |- {x} e. _V
28	27	elimak 4260	. . . . . . . . 9 |- ({x} e. (`'k(({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V)))"k Spfin ) <-> E.y e. Spfin <<y, {x}>> e. `'k(({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V))))
29	15, 27	opkelcnvk 4251	. . . . . . . . . . 11 |- (<<y, {x}>> e. `'k(({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V))) <-> <<{x}, y>> e. (({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V))))
30		vex 2863	. . . . . . . . . . . 12 |- x e. _V
31	30, 15	eqtfinrelk 4487	. . . . . . . . . . 11 |- (<<{x}, y>> e. (({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V))) <-> y = Tfin x)
32	29, 31	bitri 240	. . . . . . . . . 10 |- (<<y, {x}>> e. `'k(({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V))) <-> y = Tfin x)
33	32	rexbii 2640	. . . . . . . . 9 |- (E.y e. Spfin <<y, {x}>> e. `'k(({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V))) <-> E.y e. Spfin y = Tfin x)
34	28, 33	bitri 240	. . . . . . . 8 |- ({x} e. (`'k(({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V)))"k Spfin ) <-> E.y e. Spfin y = Tfin x)
35	30	eluni1 4174	. . . . . . . 8 |- (x e. ⋃1(`'k(({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V)))"k Spfin ) <-> {x} e. (`'k(({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V)))"k Spfin ))
36		risset 2662	. . . . . . . 8 |- ( Tfin x e. Spfin <-> E.y e. Spfin y = Tfin x)
37	34, 35, 36	3bitr4i 268	. . . . . . 7 |- (x e. ⋃1(`'k(({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V)))"k Spfin ) <-> Tfin x e. Spfin )
38	37	eqabi 2465	. . . . . 6 |- ⋃1(`'k(({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V)))"k Spfin ) = {x | Tfin x e. Spfin }
39		tfinrelkex 4488	. . . . . . . . 9 |- (({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V))) e. _V
40	39	cnvkex 4288	. . . . . . . 8 |- `'k(({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V))) e. _V
41		spfinex 4538	. . . . . . . 8 |- Spfin e. _V
42	40, 41	imakex 4301	. . . . . . 7 |- (`'k(({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V)))"k Spfin ) e. _V
43	42	uni1ex 4294	. . . . . 6 |- ⋃1(`'k(({{(/)}} X.k {(/)}) u. ( ∼ (( Ins2k Sk (+) Ins3k (( Ins3k `'k Sk \ Ins2k (( Ins2k (( Nn X.k _V) i^i (( Ins2k SIk Sk i^i Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) (+) Ins3k _I_kk )"k~P1 1c))"k~P1 1c))"k~P1 ~P1 1c) \ ({{(/)}} X.k _V)))"k Spfin ) e. _V
44	38, 43	eqeltrri 2424	. . . . 5 |- {x | Tfin x e. Spfin } e. _V
45		spfininduct 4541	. . . . 5 |- (({x | Tfin x e. Spfin } e. _V /\ Ncfin _V e. {x | Tfin x e. Spfin } /\ A.y e. Spfin A.z((y e. {x | Tfin x e. Spfin } /\ Sfin (z, y)) -> z e. {x | Tfin x e. Spfin })) -> Spfin C_ {x | Tfin x e. Spfin })
46	44, 45	mp3an1 1264	. . . 4 |- (( Ncfin _V e. {x | Tfin x e. Spfin } /\ A.y e. Spfin A.z((y e. {x | Tfin x e. Spfin } /\ Sfin (z, y)) -> z e. {x | Tfin x e. Spfin })) -> Spfin C_ {x | Tfin x e. Spfin })
47	8, 26, 46	syl2anc 642	. . 3 |- (_V e. Fin -> Spfin C_ {x | Tfin x e. Spfin })
48	47	sselda 3274	. 2 |- ((_V e. Fin /\ X e. Spfin ) -> X e. {x | Tfin x e. Spfin })
49		tfineq 4489	. . . . 5 |- (x = X -> Tfin x = Tfin X)
50	49	eleq1d 2419	. . . 4 |- (x = X -> ( Tfin x e. Spfin <-> Tfin X e. Spfin ))
51	50	elabg 2987	. . 3 |- (X e. Spfin -> (X e. {x | Tfin x e. Spfin } <-> Tfin X e. Spfin ))
52	51	adantl 452	. 2 |- ((_V e. Fin /\ X e. Spfin ) -> (X e. {x | Tfin x e. Spfin } <-> Tfin X e. Spfin ))
53	48, 52	mpbid 201	1 |- ((_V e. Fin /\ X e. Spfin ) -> Tfin X e. Spfin )

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540   = wceq 1642   e. wcel 1710  {cab 2339  A.wral 2615  E.wrex 2616  _Vcvv 2860   ∼ ccompl 3206   \ cdif 3207   u. cun 3208   i^i cin 3209   (+) csymdif 3210   C_ wss 3258  (/)c0 3551  ~Pcpw 3723  {csn 3738  <<copk 4058  ⋃₁cuni1 4134  1_cc1c 4135  ~P₁ cpw1 4136   X._k cxpk 4175  `'_kccnvk 4176   Ins2_k cins2k 4177   Ins3_k cins3k 4178  "_kcimak 4180   SI_k csik 4182   S_k cssetk 4184   _I_k_k cidk 4185   Nn cnnc 4374   Fin cfin 4377   Nc_fin cncfin 4435   T_fin ctfin 4436   S_fin wsfin 4439   Sp_fin cspfin 4440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-rab 2624  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-pss 3262  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-0c 4378  df-addc 4379  df-nnc 4380  df-fin 4381  df-ncfin 4443  df-tfin 4444  df-sfin 4447  df-spfin 4448

This theorem is referenced by:  vfinspeqtncv  4554