Metamath Proof Explorer

Theorem funimass4

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Raph Levien, 20-Nov-2006)

Ref Expression
Assertion funimass4 ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dfss2 ⊢ ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) → 𝑦 ∈ 𝐵 ) )
2 vex ⊢ 𝑦 ∈ V
3 2 elima ⊢ ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝐹 𝑦 )
4 eqcom ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑦 )
5 ssel ⊢ ( 𝐴 ⊆ dom 𝐹 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ dom 𝐹 ) )
6 funbrfvb ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐹 𝑦 ) )
7 6 ex ⊢ ( Fun 𝐹 → ( 𝑥 ∈ dom 𝐹 → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐹 𝑦 ) ) )
8 5 7 syl9 ⊢ ( 𝐴 ⊆ dom 𝐹 → ( Fun 𝐹 → ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐹 𝑦 ) ) ) )
9 8 imp31 ⊢ ( ( ( 𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐹 𝑦 ) )
10 4 9 bitrid ⊢ ( ( ( 𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 𝐹 𝑦 ) )
11 10 rexbidva ⊢ ( ( 𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹 ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝐹 𝑦 ) )
12 3 11 bitr4id ⊢ ( ( 𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹 ) → ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
13 12 imbi1d ⊢ ( ( 𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹 ) → ( ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) ) )
14 r19.23v ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) )
15 13 14 bitr4di ⊢ ( ( 𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹 ) → ( ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) ) )
16 15 albidv ⊢ ( ( 𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹 ) → ( ∀ 𝑦 ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) ) )
17 ralcom4 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) )
18 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
19 eleq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑦 ∈ 𝐵 ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
20 18 19 ceqsalv ⊢ ( ∀ 𝑦 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
21 20 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
22 17 21 bitr3i ⊢ ( ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
23 16 22 bitrdi ⊢ ( ( 𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹 ) → ( ∀ 𝑦 ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
24 1 23 bitrid ⊢ ( ( 𝐴 ⊆ dom 𝐹 ∧ Fun 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
25 24 ancoms ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )