Theorem spfininduct 4541

Description: Inductive principle for Sp_fin. Theorem X.1.51 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)

Assertion

Ref	Expression
spfininduct	⊢ ((B ∈ V ∧ Ncfin V ∈ B ∧ ∀x ∈ Spfin ∀z((x ∈ B ∧ Sfin (z, x)) → z ∈ B)) → Spfin ⊆ B)

Distinct variable group:   x,B,z

Allowed substitution hints:   V(x,z)

Proof of Theorem spfininduct

Dummy variable a is distinct from all other variables.

Step	Hyp	Ref	Expression
1		spfinex 4538	. . 3 ⊢ Spfin ∈ V
2		inexg 4101	. . 3 ⊢ (( Spfin ∈ V ∧ B ∈ V) → ( Spfin ∩ B) ∈ V)
3	1, 2	mpan 651	. 2 ⊢ (B ∈ V → ( Spfin ∩ B) ∈ V)
4		ncvspfin 4539	. . 3 ⊢ Ncfin V ∈ Spfin
5		elin 3220	. . . 4 ⊢ ( Ncfin V ∈ ( Spfin ∩ B) ↔ ( Ncfin V ∈ Spfin ∧ Ncfin V ∈ B))
6	5	biimpri 197	. . 3 ⊢ (( Ncfin V ∈ Spfin ∧ Ncfin V ∈ B) → Ncfin V ∈ ( Spfin ∩ B))
7	4, 6	mpan 651	. 2 ⊢ ( Ncfin V ∈ B → Ncfin V ∈ ( Spfin ∩ B))
8		elin 3220	. . . . 5 ⊢ (x ∈ ( Spfin ∩ B) ↔ (x ∈ Spfin ∧ x ∈ B))
9		spfinsfincl 4540	. . . . . . . . . . . . . 14 ⊢ ((x ∈ Spfin ∧ Sfin (z, x)) → z ∈ Spfin )
10	9	adantrl 696	. . . . . . . . . . . . 13 ⊢ ((x ∈ Spfin ∧ (x ∈ B ∧ Sfin (z, x))) → z ∈ Spfin )
11	10	a1d 22	. . . . . . . . . . . 12 ⊢ ((x ∈ Spfin ∧ (x ∈ B ∧ Sfin (z, x))) → (z ∈ B → z ∈ Spfin ))
12	11	ancrd 537	. . . . . . . . . . 11 ⊢ ((x ∈ Spfin ∧ (x ∈ B ∧ Sfin (z, x))) → (z ∈ B → (z ∈ Spfin ∧ z ∈ B)))
13		elin 3220	. . . . . . . . . . 11 ⊢ (z ∈ ( Spfin ∩ B) ↔ (z ∈ Spfin ∧ z ∈ B))
14	12, 13	syl6ibr 218	. . . . . . . . . 10 ⊢ ((x ∈ Spfin ∧ (x ∈ B ∧ Sfin (z, x))) → (z ∈ B → z ∈ ( Spfin ∩ B)))
15	14	ex 423	. . . . . . . . 9 ⊢ (x ∈ Spfin → ((x ∈ B ∧ Sfin (z, x)) → (z ∈ B → z ∈ ( Spfin ∩ B))))
16	15	a2d 23	. . . . . . . 8 ⊢ (x ∈ Spfin → (((x ∈ B ∧ Sfin (z, x)) → z ∈ B) → ((x ∈ B ∧ Sfin (z, x)) → z ∈ ( Spfin ∩ B))))
17	16	exp4a 589	. . . . . . 7 ⊢ (x ∈ Spfin → (((x ∈ B ∧ Sfin (z, x)) → z ∈ B) → (x ∈ B → ( Sfin (z, x) → z ∈ ( Spfin ∩ B)))))
18	17	a2i 12	. . . . . 6 ⊢ ((x ∈ Spfin → ((x ∈ B ∧ Sfin (z, x)) → z ∈ B)) → (x ∈ Spfin → (x ∈ B → ( Sfin (z, x) → z ∈ ( Spfin ∩ B)))))
19	18	imp3a 420	. . . . 5 ⊢ ((x ∈ Spfin → ((x ∈ B ∧ Sfin (z, x)) → z ∈ B)) → ((x ∈ Spfin ∧ x ∈ B) → ( Sfin (z, x) → z ∈ ( Spfin ∩ B))))
20	8, 19	syl5bi 208	. . . 4 ⊢ ((x ∈ Spfin → ((x ∈ B ∧ Sfin (z, x)) → z ∈ B)) → (x ∈ ( Spfin ∩ B) → ( Sfin (z, x) → z ∈ ( Spfin ∩ B))))
21	20	2alimi 1560	. . 3 ⊢ (∀x∀z(x ∈ Spfin → ((x ∈ B ∧ Sfin (z, x)) → z ∈ B)) → ∀x∀z(x ∈ ( Spfin ∩ B) → ( Sfin (z, x) → z ∈ ( Spfin ∩ B))))
22		df-ral 2620	. . . 4 ⊢ (∀x ∈ Spfin ∀z((x ∈ B ∧ Sfin (z, x)) → z ∈ B) ↔ ∀x(x ∈ Spfin → ∀z((x ∈ B ∧ Sfin (z, x)) → z ∈ B)))
23		19.21v 1890	. . . . 5 ⊢ (∀z(x ∈ Spfin → ((x ∈ B ∧ Sfin (z, x)) → z ∈ B)) ↔ (x ∈ Spfin → ∀z((x ∈ B ∧ Sfin (z, x)) → z ∈ B)))
24	23	albii 1566	. . . 4 ⊢ (∀x∀z(x ∈ Spfin → ((x ∈ B ∧ Sfin (z, x)) → z ∈ B)) ↔ ∀x(x ∈ Spfin → ∀z((x ∈ B ∧ Sfin (z, x)) → z ∈ B)))
25	22, 24	bitr4i 243	. . 3 ⊢ (∀x ∈ Spfin ∀z((x ∈ B ∧ Sfin (z, x)) → z ∈ B) ↔ ∀x∀z(x ∈ Spfin → ((x ∈ B ∧ Sfin (z, x)) → z ∈ B)))
26		df-ral 2620	. . . 4 ⊢ (∀x ∈ ( Spfin ∩ B)∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B)) ↔ ∀x(x ∈ ( Spfin ∩ B) → ∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B))))
27		19.21v 1890	. . . . 5 ⊢ (∀z(x ∈ ( Spfin ∩ B) → ( Sfin (z, x) → z ∈ ( Spfin ∩ B))) ↔ (x ∈ ( Spfin ∩ B) → ∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B))))
28	27	albii 1566	. . . 4 ⊢ (∀x∀z(x ∈ ( Spfin ∩ B) → ( Sfin (z, x) → z ∈ ( Spfin ∩ B))) ↔ ∀x(x ∈ ( Spfin ∩ B) → ∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B))))
29	26, 28	bitr4i 243	. . 3 ⊢ (∀x ∈ ( Spfin ∩ B)∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B)) ↔ ∀x∀z(x ∈ ( Spfin ∩ B) → ( Sfin (z, x) → z ∈ ( Spfin ∩ B))))
30	21, 25, 29	3imtr4i 257	. 2 ⊢ (∀x ∈ Spfin ∀z((x ∈ B ∧ Sfin (z, x)) → z ∈ B) → ∀x ∈ ( Spfin ∩ B)∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B)))
31		df-spfin 4448	. . . 4 ⊢ Spfin = ∩{a ∣ ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))}
32		eleq2 2414	. . . . . . . . 9 ⊢ (a = ( Spfin ∩ B) → ( Ncfin V ∈ a ↔ Ncfin V ∈ ( Spfin ∩ B)))
33		eleq2 2414	. . . . . . . . . . . 12 ⊢ (a = ( Spfin ∩ B) → (z ∈ a ↔ z ∈ ( Spfin ∩ B)))
34	33	imbi2d 307	. . . . . . . . . . 11 ⊢ (a = ( Spfin ∩ B) → (( Sfin (z, x) → z ∈ a) ↔ ( Sfin (z, x) → z ∈ ( Spfin ∩ B))))
35	34	albidv 1625	. . . . . . . . . 10 ⊢ (a = ( Spfin ∩ B) → (∀z( Sfin (z, x) → z ∈ a) ↔ ∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B))))
36	35	raleqbi1dv 2816	. . . . . . . . 9 ⊢ (a = ( Spfin ∩ B) → (∀x ∈ a ∀z( Sfin (z, x) → z ∈ a) ↔ ∀x ∈ ( Spfin ∩ B)∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B))))
37	32, 36	anbi12d 691	. . . . . . . 8 ⊢ (a = ( Spfin ∩ B) → (( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a)) ↔ ( Ncfin V ∈ ( Spfin ∩ B) ∧ ∀x ∈ ( Spfin ∩ B)∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B)))))
38	37	elabg 2987	. . . . . . 7 ⊢ (( Spfin ∩ B) ∈ V → (( Spfin ∩ B) ∈ {a ∣ ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))} ↔ ( Ncfin V ∈ ( Spfin ∩ B) ∧ ∀x ∈ ( Spfin ∩ B)∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B)))))
39	38	biimprd 214	. . . . . 6 ⊢ (( Spfin ∩ B) ∈ V → (( Ncfin V ∈ ( Spfin ∩ B) ∧ ∀x ∈ ( Spfin ∩ B)∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B))) → ( Spfin ∩ B) ∈ {a ∣ ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))}))
40	39	3impib 1149	. . . . 5 ⊢ ((( Spfin ∩ B) ∈ V ∧ Ncfin V ∈ ( Spfin ∩ B) ∧ ∀x ∈ ( Spfin ∩ B)∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B))) → ( Spfin ∩ B) ∈ {a ∣ ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))})
41		intss1 3942	. . . . 5 ⊢ (( Spfin ∩ B) ∈ {a ∣ ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))} → ∩{a ∣ ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))} ⊆ ( Spfin ∩ B))
42	40, 41	syl 15	. . . 4 ⊢ ((( Spfin ∩ B) ∈ V ∧ Ncfin V ∈ ( Spfin ∩ B) ∧ ∀x ∈ ( Spfin ∩ B)∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B))) → ∩{a ∣ ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))} ⊆ ( Spfin ∩ B))
43	31, 42	syl5eqss 3316	. . 3 ⊢ ((( Spfin ∩ B) ∈ V ∧ Ncfin V ∈ ( Spfin ∩ B) ∧ ∀x ∈ ( Spfin ∩ B)∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B))) → Spfin ⊆ ( Spfin ∩ B))
44		inss2 3477	. . 3 ⊢ ( Spfin ∩ B) ⊆ B
45	43, 44	syl6ss 3285	. 2 ⊢ ((( Spfin ∩ B) ∈ V ∧ Ncfin V ∈ ( Spfin ∩ B) ∧ ∀x ∈ ( Spfin ∩ B)∀z( Sfin (z, x) → z ∈ ( Spfin ∩ B))) → Spfin ⊆ B)
46	3, 7, 30, 45	syl3an 1224	1 ⊢ ((B ∈ V ∧ Ncfin V ∈ B ∧ ∀x ∈ Spfin ∀z((x ∈ B ∧ Sfin (z, x)) → z ∈ B)) → Spfin ⊆ B)

Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934  ∀wal 1540   = wceq 1642   ∈ wcel 1710  {cab 2339  ∀wral 2615  Vcvv 2860   ∩ cin 3209   ⊆ wss 3258  ∩cint 3927   Nc_fin cncfin 4435   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-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-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  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-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-iota 4340  df-addc 4379  df-nnc 4380  df-ncfin 4443  df-sfin 4447  df-spfin 4448

This theorem is referenced by:  vfinspnn  4542  vfinspss  4552  vfinspclt  4553