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

Theorem spfinsfincl 4539
 Description: If X is in Spfin and Z is smaller than X, then Z is also in Spfin. Theorem X.1.50 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
Assertion
Ref Expression
spfinsfincl ((X Spfin Sfin (Z, X)) → Z Spfin )

Proof of Theorem spfinsfincl
Dummy variables p a q x z y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sfin 4446 . . . 4 ( Sfin (Z, X) ↔ (Z Nn X Nn y(1y Z y X)))
2 sfineq1 4526 . . . . . . 7 (z = Z → ( Sfin (z, x) ↔ Sfin (Z, x)))
3 eleq1 2413 . . . . . . . 8 (z = Z → (z SpfinZ Spfin ))
43imbi2d 307 . . . . . . 7 (z = Z → ((x Spfinz Spfin ) ↔ (x SpfinZ Spfin )))
52, 4imbi12d 311 . . . . . 6 (z = Z → (( Sfin (z, x) → (x Spfinz Spfin )) ↔ ( Sfin (Z, x) → (x SpfinZ Spfin ))))
6 sfineq2 4527 . . . . . . 7 (x = X → ( Sfin (Z, x) ↔ Sfin (Z, X)))
7 eleq1 2413 . . . . . . . 8 (x = X → (x SpfinX Spfin ))
87imbi1d 308 . . . . . . 7 (x = X → ((x SpfinZ Spfin ) ↔ (X SpfinZ Spfin )))
96, 8imbi12d 311 . . . . . 6 (x = X → (( Sfin (Z, x) → (x SpfinZ Spfin )) ↔ ( Sfin (Z, X) → (X SpfinZ Spfin ))))
10 sfineq2 4527 . . . . . . . . . . . . . . 15 (p = x → ( Sfin (q, p) ↔ Sfin (q, x)))
1110imbi1d 308 . . . . . . . . . . . . . 14 (p = x → (( Sfin (q, p) → q a) ↔ ( Sfin (q, x) → q a)))
1211albidv 1625 . . . . . . . . . . . . 13 (p = x → (q( Sfin (q, p) → q a) ↔ q( Sfin (q, x) → q a)))
1312rspcv 2951 . . . . . . . . . . . 12 (x a → (p a q( Sfin (q, p) → q a) → q( Sfin (q, x) → q a)))
14 sfineq1 4526 . . . . . . . . . . . . . . 15 (q = z → ( Sfin (q, x) ↔ Sfin (z, x)))
15 eleq1 2413 . . . . . . . . . . . . . . 15 (q = z → (q az a))
1614, 15imbi12d 311 . . . . . . . . . . . . . 14 (q = z → (( Sfin (q, x) → q a) ↔ ( Sfin (z, x) → z a)))
1716spv 1998 . . . . . . . . . . . . 13 (q( Sfin (q, x) → q a) → ( Sfin (z, x) → z a))
1817com12 27 . . . . . . . . . . . 12 ( Sfin (z, x) → (q( Sfin (q, x) → q a) → z a))
1913, 18syl9r 67 . . . . . . . . . . 11 ( Sfin (z, x) → (x a → (p a q( Sfin (q, p) → q a) → z a)))
2019com23 72 . . . . . . . . . 10 ( Sfin (z, x) → (p a q( Sfin (q, p) → q a) → (x az a)))
2120adantld 453 . . . . . . . . 9 ( Sfin (z, x) → (( Ncfin V a p a q( Sfin (q, p) → q a)) → (x az a)))
2221a2d 23 . . . . . . . 8 ( Sfin (z, x) → ((( Ncfin V a p a q( Sfin (q, p) → q a)) → x a) → (( Ncfin V a p a q( Sfin (q, p) → q a)) → z a)))
2322alimdv 1621 . . . . . . 7 ( Sfin (z, x) → (a(( Ncfin V a p a q( Sfin (q, p) → q a)) → x a) → a(( Ncfin V a p a q( Sfin (q, p) → q a)) → z a)))
24 df-spfin 4447 . . . . . . . . 9 Spfin = {a ( Ncfin V a p a q( Sfin (q, p) → q a))}
2524eleq2i 2417 . . . . . . . 8 (x Spfinx {a ( Ncfin V a p a q( Sfin (q, p) → q a))})
26 vex 2862 . . . . . . . . 9 x V
2726elintab 3937 . . . . . . . 8 (x {a ( Ncfin V a p a q( Sfin (q, p) → q a))} ↔ a(( Ncfin V a p a q( Sfin (q, p) → q a)) → x a))
2825, 27bitri 240 . . . . . . 7 (x Spfina(( Ncfin V a p a q( Sfin (q, p) → q a)) → x a))
2924eleq2i 2417 . . . . . . . 8 (z Spfinz {a ( Ncfin V a p a q( Sfin (q, p) → q a))})
30 vex 2862 . . . . . . . . 9 z V
3130elintab 3937 . . . . . . . 8 (z {a ( Ncfin V a p a q( Sfin (q, p) → q a))} ↔ a(( Ncfin V a p a q( Sfin (q, p) → q a)) → z a))
3229, 31bitri 240 . . . . . . 7 (z Spfina(( Ncfin V a p a q( Sfin (q, p) → q a)) → z a))
3323, 28, 323imtr4g 261 . . . . . 6 ( Sfin (z, x) → (x Spfinz Spfin ))
345, 9, 33vtocl2g 2918 . . . . 5 ((Z Nn X Nn ) → ( Sfin (Z, X) → (X SpfinZ Spfin )))
35343adant3 975 . . . 4 ((Z Nn X Nn y(1y Z y X)) → ( Sfin (Z, X) → (X SpfinZ Spfin )))
361, 35sylbi 187 . . 3 ( Sfin (Z, X) → ( Sfin (Z, X) → (X SpfinZ Spfin )))
3736pm2.43i 43 . 2 ( Sfin (Z, X) → (X SpfinZ Spfin ))
3837impcom 419 1 ((X Spfin Sfin (Z, X)) → Z Spfin )
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  ∀wral 2614  Vcvv 2859  ℘cpw 3722  ∩cint 3926  ℘1cpw1 4135   Nn cnnc 4373   Ncfin cncfin 4434   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-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  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-ral 2619  df-v 2861  df-int 3927  df-sfin 4446  df-spfin 4447 This theorem is referenced by:  spfininduct  4540  1cspfin  4543  vfinspsslem1  4550  vfinspclt  4552
 Copyright terms: Public domain W3C validator