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

Theorem vfinspclt 4552
 Description: If the universe is finite, then Spfin is closed under T-raising. Theorem X.1.60 of [Rosser] p. 536. (Contributed by SF, 30-Jan-2015.)
Assertion
Ref Expression
vfinspclt ((V Fin X Spfin ) → Tfin X Spfin )

Proof of Theorem vfinspclt
Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tncveqnc1fin 4544 . . . . . 6 (V FinTfin Ncfin V = Ncfin 1c)
2 1cspfin 4543 . . . . . 6 (V FinNcfin 1c Spfin )
31, 2eqeltrd 2427 . . . . 5 (V FinTfin Ncfin V Spfin )
4 ncfinex 4472 . . . . . 6 Ncfin V V
5 tfineq 4488 . . . . . . 7 (x = Ncfin V → Tfin x = Tfin Ncfin V)
65eleq1d 2419 . . . . . 6 (x = Ncfin V → ( Tfin x SpfinTfin Ncfin V Spfin ))
74, 6elab 2985 . . . . 5 ( Ncfin V {x Tfin x Spfin } ↔ Tfin Ncfin V Spfin )
83, 7sylibr 203 . . . 4 (V FinNcfin V {x Tfin x Spfin })
9 simprl 732 . . . . . . . . 9 (((V Fin y Spfin ) ( Tfin y Spfin Sfin (z, y))) → Tfin y Spfin )
10 sfintfin 4532 . . . . . . . . . 10 ( Sfin (z, y) → Sfin ( Tfin z, Tfin y))
1110ad2antll 709 . . . . . . . . 9 (((V Fin y Spfin ) ( Tfin y Spfin Sfin (z, y))) → Sfin ( Tfin z, Tfin y))
12 spfinsfincl 4539 . . . . . . . . 9 (( Tfin y Spfin Sfin ( Tfin z, Tfin y)) → Tfin z Spfin )
139, 11, 12syl2anc 642 . . . . . . . 8 (((V Fin y Spfin ) ( Tfin y Spfin Sfin (z, y))) → Tfin z Spfin )
1413ex 423 . . . . . . 7 ((V Fin y Spfin ) → (( Tfin y Spfin Sfin (z, y)) → Tfin z Spfin ))
15 vex 2862 . . . . . . . . 9 y V
16 tfineq 4488 . . . . . . . . . 10 (x = yTfin x = Tfin y)
1716eleq1d 2419 . . . . . . . . 9 (x = y → ( Tfin x SpfinTfin y Spfin ))
1815, 17elab 2985 . . . . . . . 8 (y {x Tfin x Spfin } ↔ Tfin y Spfin )
1918anbi1i 676 . . . . . . 7 ((y {x Tfin x Spfin } Sfin (z, y)) ↔ ( Tfin y Spfin Sfin (z, y)))
20 vex 2862 . . . . . . . 8 z V
21 tfineq 4488 . . . . . . . . 9 (x = zTfin x = Tfin z)
2221eleq1d 2419 . . . . . . . 8 (x = z → ( Tfin x SpfinTfin z Spfin ))
2320, 22elab 2985 . . . . . . 7 (z {x Tfin x Spfin } ↔ Tfin z Spfin )
2414, 19, 233imtr4g 261 . . . . . 6 ((V Fin y Spfin ) → ((y {x Tfin x Spfin } Sfin (z, y)) → z {x Tfin x Spfin }))
2524alrimiv 1631 . . . . 5 ((V Fin y Spfin ) → z((y {x Tfin x Spfin } Sfin (z, y)) → z {x Tfin x Spfin }))
2625ralrimiva 2697 . . . 4 (V Finy Spfin z((y {x Tfin x Spfin } Sfin (z, y)) → z {x Tfin x Spfin }))
27 snex 4111 . . . . . . . . . 10 {x} V
2827elimak 4259 . . . . . . . . 9 ({x} (k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) “k Spfin ) ↔ y Spfiny, {x}⟫ k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))))
2915, 27opkelcnvk 4250 . . . . . . . . . . 11 (⟪y, {x}⟫ k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ ⟪{x}, y (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))))
30 vex 2862 . . . . . . . . . . . 12 x V
3130, 15eqtfinrelk 4486 . . . . . . . . . . 11 (⟪{x}, y (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ y = Tfin x)
3229, 31bitri 240 . . . . . . . . . 10 (⟪y, {x}⟫ k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ y = Tfin x)
3332rexbii 2639 . . . . . . . . 9 (y Spfiny, {x}⟫ k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ y Spfin y = Tfin x)
3428, 33bitri 240 . . . . . . . 8 ({x} (k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) “k Spfin ) ↔ y Spfin y = Tfin x)
3530eluni1 4173 . . . . . . . 8 (x 1(k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) “k Spfin ) ↔ {x} (k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) “k Spfin ))
36 risset 2661 . . . . . . . 8 ( Tfin x Spfiny Spfin y = Tfin x)
3734, 35, 363bitr4i 268 . . . . . . 7 (x 1(k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) “k Spfin ) ↔ Tfin x Spfin )
3837abbi2i 2464 . . . . . 6 1(k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) “k Spfin ) = {x Tfin x Spfin }
39 tfinrelkex 4487 . . . . . . . . 9 (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) V
4039cnvkex 4287 . . . . . . . 8 k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) V
41 spfinex 4537 . . . . . . . 8 Spfin V
4240, 41imakex 4300 . . . . . . 7 (k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) “k Spfin ) V
4342uni1ex 4293 . . . . . 6 1(k(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) “k Spfin ) V
4438, 43eqeltrri 2424 . . . . 5 {x Tfin x Spfin } V
45 spfininduct 4540 . . . . 5 (({x Tfin x Spfin } V Ncfin V {x Tfin x Spfin } y Spfin z((y {x Tfin x Spfin } Sfin (z, y)) → z {x Tfin x Spfin })) → Spfin {x Tfin x Spfin })
4644, 45mp3an1 1264 . . . 4 (( Ncfin V {x Tfin x Spfin } y Spfin z((y {x Tfin x Spfin } Sfin (z, y)) → z {x Tfin x Spfin })) → Spfin {x Tfin x Spfin })
478, 26, 46syl2anc 642 . . 3 (V FinSpfin {x Tfin x Spfin })
4847sselda 3273 . 2 ((V Fin X Spfin ) → X {x Tfin x Spfin })
49 tfineq 4488 . . . . 5 (x = XTfin x = Tfin X)
5049eleq1d 2419 . . . 4 (x = X → ( Tfin x SpfinTfin X Spfin ))
5150elabg 2986 . . 3 (X Spfin → (X {x Tfin x Spfin } ↔ Tfin X Spfin ))
5251adantl 452 . 2 ((V Fin X Spfin ) → (X {x Tfin x Spfin } ↔ Tfin X Spfin ))
5348, 52mpbid 201 1 ((V Fin X Spfin ) → Tfin X Spfin )
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540   = wceq 1642   ∈ wcel 1710  {cab 2339  ∀wral 2614  ∃wrex 2615  Vcvv 2859   ∼ ccompl 3205   ∖ cdif 3206   ∪ cun 3207   ∩ cin 3208   ⊕ csymdif 3209   ⊆ wss 3257  ∅c0 3550  ℘cpw 3722  {csn 3737  ⟪copk 4057  ⋃1cuni1 4133  1cc1c 4134  ℘1cpw1 4135   ×k cxpk 4174  ◡kccnvk 4175   Ins2k cins2k 4176   Ins3k cins3k 4177   “k cimak 4179   SIk csik 4181   Sk cssetk 4183   Ik cidk 4184   Nn cnnc 4373   Fin cfin 4376   Ncfin cncfin 4434   Tfin ctfin 4435   Sfin wsfin 4438   Spfin cspfin 4439 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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-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-ncfin 4442  df-tfin 4443  df-sfin 4446  df-spfin 4447 This theorem is referenced by:  vfinspeqtncv  4553
 Copyright terms: Public domain W3C validator