Theorem imainss

Description: An upper bound for intersection with an image. Theorem 41 of Suppes p. 66. (Contributed by NM, 11-Aug-2004)

	Ref	Expression
Assertion	imainss	⊢ ( ( 𝑅 “ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑅 “ ( 𝐴 ∩ ( ◡ 𝑅 “ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑦 ∈ V
2		vex	⊢ 𝑥 ∈ V
3	1 2	brcnv	⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
4		19.8a	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ◡ 𝑅 𝑥 ) → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ◡ 𝑅 𝑥 ) )
5	3 4	sylan2br	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝑅 𝑦 ) → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ◡ 𝑅 𝑥 ) )
6	5	ancoms	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ◡ 𝑅 𝑥 ) )
7	6	anim2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ◡ 𝑅 𝑥 ) ) )
8		simprl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 𝑅 𝑦 )
9	7 8	jca	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ◡ 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) )
10	9	anassrs	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ◡ 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) )
11		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( ◡ 𝑅 “ 𝐵 ) ) )
12	2	elima2	⊢ ( 𝑥 ∈ ( ◡ 𝑅 “ 𝐵 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ◡ 𝑅 𝑥 ) )
13	12	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( ◡ 𝑅 “ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ◡ 𝑅 𝑥 ) ) )
14	11 13	bitri	⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ◡ 𝑅 𝑥 ) ) )
15	14	anbi1i	⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ 𝐵 ) ) ∧ 𝑥 𝑅 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ◡ 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) )
16	10 15	sylibr	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ 𝐵 ) ) ∧ 𝑥 𝑅 𝑦 ) )
17	16	eximi	⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ( 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ 𝐵 ) ) ∧ 𝑥 𝑅 𝑦 ) )
18	1	elima2	⊢ ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) )
19	18	anbi1i	⊢ ( ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ∧ 𝑦 ∈ 𝐵 ) )
20		elin	⊢ ( 𝑦 ∈ ( ( 𝑅 “ 𝐴 ) ∩ 𝐵 ) ↔ ( 𝑦 ∈ ( 𝑅 “ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) )
21		19.41v	⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ∧ 𝑦 ∈ 𝐵 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ∧ 𝑦 ∈ 𝐵 ) )
22	19 20 21	3bitr4i	⊢ ( 𝑦 ∈ ( ( 𝑅 “ 𝐴 ) ∩ 𝐵 ) ↔ ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ∧ 𝑦 ∈ 𝐵 ) )
23	1	elima2	⊢ ( 𝑦 ∈ ( 𝑅 “ ( 𝐴 ∩ ( ◡ 𝑅 “ 𝐵 ) ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ 𝐵 ) ) ∧ 𝑥 𝑅 𝑦 ) )
24	17 22 23	3imtr4i	⊢ ( 𝑦 ∈ ( ( 𝑅 “ 𝐴 ) ∩ 𝐵 ) → 𝑦 ∈ ( 𝑅 “ ( 𝐴 ∩ ( ◡ 𝑅 “ 𝐵 ) ) ) )
25	24	ssriv	⊢ ( ( 𝑅 “ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑅 “ ( 𝐴 ∩ ( ◡ 𝑅 “ 𝐵 ) ) )