This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnfi

Description: A version of fnex for finite sets that does not require Replacement or Power Sets. (Contributed by Mario Carneiro, 16-Nov-2014) (Revised by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion fnfi ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → 𝐹 ∈ Fin )

Proof

Step Hyp Ref Expression
1 fnresdm ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
2 1 adantr ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
3 reseq2 ⊢ ( 𝑥 = ∅ → ( 𝐹 ↾ 𝑥 ) = ( 𝐹 ↾ ∅ ) )
4 3 eleq1d ⊢ ( 𝑥 = ∅ → ( ( 𝐹 ↾ 𝑥 ) ∈ Fin ↔ ( 𝐹 ↾ ∅ ) ∈ Fin ) )
5 4 imbi2d ⊢ ( 𝑥 = ∅ → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝑥 ) ∈ Fin ) ↔ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ ∅ ) ∈ Fin ) ) )
6 reseq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ↾ 𝑥 ) = ( 𝐹 ↾ 𝑦 ) )
7 6 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ↾ 𝑥 ) ∈ Fin ↔ ( 𝐹 ↾ 𝑦 ) ∈ Fin ) )
8 7 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝑥 ) ∈ Fin ) ↔ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝑦 ) ∈ Fin ) ) )
9 reseq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐹 ↾ 𝑥 ) = ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) )
10 9 eleq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐹 ↾ 𝑥 ) ∈ Fin ↔ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
11 10 imbi2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝑥 ) ∈ Fin ) ↔ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) ) )
12 reseq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ↾ 𝑥 ) = ( 𝐹 ↾ 𝐴 ) )
13 12 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ↾ 𝑥 ) ∈ Fin ↔ ( 𝐹 ↾ 𝐴 ) ∈ Fin ) )
14 13 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝑥 ) ∈ Fin ) ↔ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝐴 ) ∈ Fin ) ) )
15 res0 ⊢ ( 𝐹 ↾ ∅ ) = ∅
16 0fi ⊢ ∅ ∈ Fin
17 15 16 eqeltri ⊢ ( 𝐹 ↾ ∅ ) ∈ Fin
18 17 a1i ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ ∅ ) ∈ Fin )
19 resundi ⊢ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( 𝐹 ↾ 𝑦 ) ∪ ( 𝐹 ↾ { 𝑧 } ) )
20 snfi ⊢ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } ∈ Fin
21 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
22 funressn ⊢ ( Fun 𝐹 → ( 𝐹 ↾ { 𝑧 } ) ⊆ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } )
23 21 22 syl ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ { 𝑧 } ) ⊆ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } )
24 23 adantr ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ { 𝑧 } ) ⊆ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } )
25 ssfi ⊢ ( ( { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } ∈ Fin ∧ ( 𝐹 ↾ { 𝑧 } ) ⊆ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } ) → ( 𝐹 ↾ { 𝑧 } ) ∈ Fin )
26 20 24 25 sylancr ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ { 𝑧 } ) ∈ Fin )
27 unfi ⊢ ( ( ( 𝐹 ↾ 𝑦 ) ∈ Fin ∧ ( 𝐹 ↾ { 𝑧 } ) ∈ Fin ) → ( ( 𝐹 ↾ 𝑦 ) ∪ ( 𝐹 ↾ { 𝑧 } ) ) ∈ Fin )
28 26 27 sylan2 ⊢ ( ( ( 𝐹 ↾ 𝑦 ) ∈ Fin ∧ ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) ) → ( ( 𝐹 ↾ 𝑦 ) ∪ ( 𝐹 ↾ { 𝑧 } ) ) ∈ Fin )
29 19 28 eqeltrid ⊢ ( ( ( 𝐹 ↾ 𝑦 ) ∈ Fin ∧ ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) ) → ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
30 29 expcom ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( ( 𝐹 ↾ 𝑦 ) ∈ Fin → ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
31 30 a2i ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝑦 ) ∈ Fin ) → ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
32 31 a1i ⊢ ( 𝑦 ∈ Fin → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝑦 ) ∈ Fin ) → ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) ) )
33 5 8 11 14 18 32 findcard2 ⊢ ( 𝐴 ∈ Fin → ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝐴 ) ∈ Fin ) )
34 33 anabsi7 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝐴 ) ∈ Fin )
35 2 34 eqeltrrd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → 𝐹 ∈ Fin )