Metamath Proof Explorer

Theorem imafiOLD

Description: Obsolete version of imafi as of 25-Jun-2025. (Contributed by Stefan O'Rear, 22-Feb-2015) Avoid ax-pow . (Revised by BTernaryTau, 7-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion imafiOLD ( ( Fun 𝐹 ∧ 𝑋 ∈ Fin ) → ( 𝐹 “ 𝑋 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 imaeq2 ⊢ ( 𝑥 = ∅ → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ∅ ) )
2 1 eleq1d ⊢ ( 𝑥 = ∅ → ( ( 𝐹 “ 𝑥 ) ∈ Fin ↔ ( 𝐹 “ ∅ ) ∈ Fin ) )
3 2 imbi2d ⊢ ( 𝑥 = ∅ → ( ( Fun 𝐹 → ( 𝐹 “ 𝑥 ) ∈ Fin ) ↔ ( Fun 𝐹 → ( 𝐹 “ ∅ ) ∈ Fin ) ) )
4 imaeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑦 ) )
5 4 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 “ 𝑥 ) ∈ Fin ↔ ( 𝐹 “ 𝑦 ) ∈ Fin ) )
6 5 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( Fun 𝐹 → ( 𝐹 “ 𝑥 ) ∈ Fin ) ↔ ( Fun 𝐹 → ( 𝐹 “ 𝑦 ) ∈ Fin ) ) )
7 imaeq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) )
8 7 eleq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐹 “ 𝑥 ) ∈ Fin ↔ ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
9 8 imbi2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( Fun 𝐹 → ( 𝐹 “ 𝑥 ) ∈ Fin ) ↔ ( Fun 𝐹 → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) ) )
10 imaeq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑋 ) )
11 10 eleq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 “ 𝑥 ) ∈ Fin ↔ ( 𝐹 “ 𝑋 ) ∈ Fin ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝑋 → ( ( Fun 𝐹 → ( 𝐹 “ 𝑥 ) ∈ Fin ) ↔ ( Fun 𝐹 → ( 𝐹 “ 𝑋 ) ∈ Fin ) ) )
13 ima0 ⊢ ( 𝐹 “ ∅ ) = ∅
14 0fi ⊢ ∅ ∈ Fin
15 13 14 eqeltri ⊢ ( 𝐹 “ ∅ ) ∈ Fin
16 15 a1i ⊢ ( Fun 𝐹 → ( 𝐹 “ ∅ ) ∈ Fin )
17 funfn ⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
18 fnsnfv ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → { ( 𝐹 ‘ 𝑧 ) } = ( 𝐹 “ { 𝑧 } ) )
19 17 18 sylanb ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → { ( 𝐹 ‘ 𝑧 ) } = ( 𝐹 “ { 𝑧 } ) )
20 snfi ⊢ { ( 𝐹 ‘ 𝑧 ) } ∈ Fin
21 19 20 eqeltrrdi ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 “ { 𝑧 } ) ∈ Fin )
22 ndmima ⊢ ( ¬ 𝑧 ∈ dom 𝐹 → ( 𝐹 “ { 𝑧 } ) = ∅ )
23 22 14 eqeltrdi ⊢ ( ¬ 𝑧 ∈ dom 𝐹 → ( 𝐹 “ { 𝑧 } ) ∈ Fin )
24 23 adantl ⊢ ( ( Fun 𝐹 ∧ ¬ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 “ { 𝑧 } ) ∈ Fin )
25 21 24 pm2.61dan ⊢ ( Fun 𝐹 → ( 𝐹 “ { 𝑧 } ) ∈ Fin )
26 imaundi ⊢ ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( 𝐹 “ 𝑦 ) ∪ ( 𝐹 “ { 𝑧 } ) )
27 unfi ⊢ ( ( ( 𝐹 “ 𝑦 ) ∈ Fin ∧ ( 𝐹 “ { 𝑧 } ) ∈ Fin ) → ( ( 𝐹 “ 𝑦 ) ∪ ( 𝐹 “ { 𝑧 } ) ) ∈ Fin )
28 26 27 eqeltrid ⊢ ( ( ( 𝐹 “ 𝑦 ) ∈ Fin ∧ ( 𝐹 “ { 𝑧 } ) ∈ Fin ) → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
29 25 28 sylan2 ⊢ ( ( ( 𝐹 “ 𝑦 ) ∈ Fin ∧ Fun 𝐹 ) → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
30 29 expcom ⊢ ( Fun 𝐹 → ( ( 𝐹 “ 𝑦 ) ∈ Fin → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
31 30 a2i ⊢ ( ( Fun 𝐹 → ( 𝐹 “ 𝑦 ) ∈ Fin ) → ( Fun 𝐹 → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
32 31 a1i ⊢ ( 𝑦 ∈ Fin → ( ( Fun 𝐹 → ( 𝐹 “ 𝑦 ) ∈ Fin ) → ( Fun 𝐹 → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) ) )
33 3 6 9 12 16 32 findcard2 ⊢ ( 𝑋 ∈ Fin → ( Fun 𝐹 → ( 𝐹 “ 𝑋 ) ∈ Fin ) )
34 33 impcom ⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ Fin ) → ( 𝐹 “ 𝑋 ) ∈ Fin )