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 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑋 ∈ ∩ ( 𝐹 “ 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐵 𝑋 ∈ ( 𝐹 ‘ 𝑦 ) ) )