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

Metamath Proof Explorer

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 ⊢ ( ( 𝑅 “ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑅 “ ( 𝐴 ∩ ( ◡ 𝑅 “ 𝐵 ) ) )