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

Metamath Proof Explorer

Theorem elintfv

Description: Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021)

Ref Expression
Hypothesis elintfv.1 ⊢ 𝑋 ∈ V
Assertion elintfv ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑋 ∈ ∩ ( 𝐹 “ 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐵 𝑋 ∈ ( 𝐹 ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 elintfv.1 ⊢ 𝑋 ∈ V
2 1 elint ⊢ ( 𝑋 ∈ ∩ ( 𝐹 “ 𝐵 ) ↔ ∀ 𝑧 ( 𝑧 ∈ ( 𝐹 “ 𝐵 ) → 𝑋 ∈ 𝑧 ) )
3 fvelimab ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑧 ) )
4 3 imbi1d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑧 ∈ ( 𝐹 “ 𝐵 ) → 𝑋 ∈ 𝑧 ) ↔ ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑧 → 𝑋 ∈ 𝑧 ) ) )
5 r19.23v ⊢ ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → 𝑋 ∈ 𝑧 ) ↔ ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑧 → 𝑋 ∈ 𝑧 ) )
6 4 5 bitr4di ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑧 ∈ ( 𝐹 “ 𝐵 ) → 𝑋 ∈ 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → 𝑋 ∈ 𝑧 ) ) )
7 6 albidv ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑧 ( 𝑧 ∈ ( 𝐹 “ 𝐵 ) → 𝑋 ∈ 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → 𝑋 ∈ 𝑧 ) ) )
8 ralcom4 ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → 𝑋 ∈ 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → 𝑋 ∈ 𝑧 ) )
9 eqcom ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑧 ↔ 𝑧 = ( 𝐹 ‘ 𝑦 ) )
10 9 imbi1i ⊢ ( ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → 𝑋 ∈ 𝑧 ) ↔ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → 𝑋 ∈ 𝑧 ) )
11 10 albii ⊢ ( ∀ 𝑧 ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → 𝑋 ∈ 𝑧 ) ↔ ∀ 𝑧 ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → 𝑋 ∈ 𝑧 ) )
12 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
13 eleq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → ( 𝑋 ∈ 𝑧 ↔ 𝑋 ∈ ( 𝐹 ‘ 𝑦 ) ) )
14 12 13 ceqsalv ⊢ ( ∀ 𝑧 ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → 𝑋 ∈ 𝑧 ) ↔ 𝑋 ∈ ( 𝐹 ‘ 𝑦 ) )
15 11 14 bitri ⊢ ( ∀ 𝑧 ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → 𝑋 ∈ 𝑧 ) ↔ 𝑋 ∈ ( 𝐹 ‘ 𝑦 ) )
16 15 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → 𝑋 ∈ 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐵 𝑋 ∈ ( 𝐹 ‘ 𝑦 ) )
17 8 16 bitr3i ⊢ ( ∀ 𝑧 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → 𝑋 ∈ 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐵 𝑋 ∈ ( 𝐹 ‘ 𝑦 ) )
18 7 17 bitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑧 ( 𝑧 ∈ ( 𝐹 “ 𝐵 ) → 𝑋 ∈ 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐵 𝑋 ∈ ( 𝐹 ‘ 𝑦 ) ) )
19 2 18 bitrid ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑋 ∈ ∩ ( 𝐹 “ 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐵 𝑋 ∈ ( 𝐹 ‘ 𝑦 ) ) )