Theorem ssfiALT

Description: Shorter proof of ssfi using ax-pow . (Contributed by NM, 24-Jun-1998) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ssfiALT	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		isfi	⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
2		bren	⊢ ( 𝐴 ≈ 𝑥 ↔ ∃ 𝑧 𝑧 : 𝐴 –1-1-onto→ 𝑥 )
3		f1ofo	⊢ ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 → 𝑧 : 𝐴 –onto→ 𝑥 )
4		imassrn	⊢ ( 𝑧 “ 𝐵 ) ⊆ ran 𝑧
5		forn	⊢ ( 𝑧 : 𝐴 –onto→ 𝑥 → ran 𝑧 = 𝑥 )
6	4 5	sseqtrid	⊢ ( 𝑧 : 𝐴 –onto→ 𝑥 → ( 𝑧 “ 𝐵 ) ⊆ 𝑥 )
7	3 6	syl	⊢ ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑧 “ 𝐵 ) ⊆ 𝑥 )
8		ssnnfi	⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑧 “ 𝐵 ) ⊆ 𝑥 ) → ( 𝑧 “ 𝐵 ) ∈ Fin )
9		isfi	⊢ ( ( 𝑧 “ 𝐵 ) ∈ Fin ↔ ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 )
10	8 9	sylib	⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑧 “ 𝐵 ) ⊆ 𝑥 ) → ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 )
11	7 10	sylan2	⊢ ( ( 𝑥 ∈ ω ∧ 𝑧 : 𝐴 –1-1-onto→ 𝑥 ) → ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 )
12	11	adantrr	⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) ) → ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 )
13		f1of1	⊢ ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 → 𝑧 : 𝐴 –1-1→ 𝑥 )
14		f1ores	⊢ ( ( 𝑧 : 𝐴 –1-1→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑧 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) )
15	13 14	sylan	⊢ ( ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑧 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) )
16		vex	⊢ 𝑧 ∈ V
17	16	resex	⊢ ( 𝑧 ↾ 𝐵 ) ∈ V
18		f1oeq1	⊢ ( 𝑥 = ( 𝑧 ↾ 𝐵 ) → ( 𝑥 : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) ↔ ( 𝑧 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) ) )
19	17 18	spcev	⊢ ( ( 𝑧 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) → ∃ 𝑥 𝑥 : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) )
20		bren	⊢ ( 𝐵 ≈ ( 𝑧 “ 𝐵 ) ↔ ∃ 𝑥 𝑥 : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) )
21	19 20	sylibr	⊢ ( ( 𝑧 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) → 𝐵 ≈ ( 𝑧 “ 𝐵 ) )
22		entr	⊢ ( ( 𝐵 ≈ ( 𝑧 “ 𝐵 ) ∧ ( 𝑧 “ 𝐵 ) ≈ 𝑦 ) → 𝐵 ≈ 𝑦 )
23	21 22	sylan	⊢ ( ( ( 𝑧 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) ∧ ( 𝑧 “ 𝐵 ) ≈ 𝑦 ) → 𝐵 ≈ 𝑦 )
24	15 23	sylan	⊢ ( ( ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑧 “ 𝐵 ) ≈ 𝑦 ) → 𝐵 ≈ 𝑦 )
25	24	ex	⊢ ( ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑧 “ 𝐵 ) ≈ 𝑦 → 𝐵 ≈ 𝑦 ) )
26	25	reximdv	⊢ ( ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 → ∃ 𝑦 ∈ ω 𝐵 ≈ 𝑦 ) )
27		isfi	⊢ ( 𝐵 ∈ Fin ↔ ∃ 𝑦 ∈ ω 𝐵 ≈ 𝑦 )
28	26 27	imbitrrdi	⊢ ( ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 → 𝐵 ∈ Fin ) )
29	28	adantl	⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) ) → ( ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 → 𝐵 ∈ Fin ) )
30	12 29	mpd	⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐵 ∈ Fin )
31	30	exp32	⊢ ( 𝑥 ∈ ω → ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin ) ) )
32	31	exlimdv	⊢ ( 𝑥 ∈ ω → ( ∃ 𝑧 𝑧 : 𝐴 –1-1-onto→ 𝑥 → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin ) ) )
33	2 32	biimtrid	⊢ ( 𝑥 ∈ ω → ( 𝐴 ≈ 𝑥 → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin ) ) )
34	33	rexlimiv	⊢ ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin ) )
35	1 34	sylbi	⊢ ( 𝐴 ∈ Fin → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin ) )
36	35	imp	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin )