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

Metamath Proof Explorer

Theorem elima4

Description: Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018)

Ref Expression
Assertion elima4 ( 𝐴 ∈ ( 𝑅 “ 𝐵 ) ↔ ( 𝑅 ∩ ( 𝐵 × { 𝐴 } ) ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ ( 𝑅 “ 𝐵 ) → 𝐴 ∈ V )
2 xpeq2 ⊢ ( { 𝐴 } = ∅ → ( 𝐵 × { 𝐴 } ) = ( 𝐵 × ∅ ) )
3 xp0 ⊢ ( 𝐵 × ∅ ) = ∅
4 2 3 eqtrdi ⊢ ( { 𝐴 } = ∅ → ( 𝐵 × { 𝐴 } ) = ∅ )
5 4 ineq2d ⊢ ( { 𝐴 } = ∅ → ( 𝑅 ∩ ( 𝐵 × { 𝐴 } ) ) = ( 𝑅 ∩ ∅ ) )
6 in0 ⊢ ( 𝑅 ∩ ∅ ) = ∅
7 5 6 eqtrdi ⊢ ( { 𝐴 } = ∅ → ( 𝑅 ∩ ( 𝐵 × { 𝐴 } ) ) = ∅ )
8 7 necon3i ⊢ ( ( 𝑅 ∩ ( 𝐵 × { 𝐴 } ) ) ≠ ∅ → { 𝐴 } ≠ ∅ )
9 snnzb ⊢ ( 𝐴 ∈ V ↔ { 𝐴 } ≠ ∅ )
10 8 9 sylibr ⊢ ( ( 𝑅 ∩ ( 𝐵 × { 𝐴 } ) ) ≠ ∅ → 𝐴 ∈ V )
11 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ( 𝑅 “ 𝐵 ) ↔ 𝐴 ∈ ( 𝑅 “ 𝐵 ) ) )
12 sneq ⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
13 12 xpeq2d ⊢ ( 𝑥 = 𝐴 → ( 𝐵 × { 𝑥 } ) = ( 𝐵 × { 𝐴 } ) )
14 13 ineq2d ⊢ ( 𝑥 = 𝐴 → ( 𝑅 ∩ ( 𝐵 × { 𝑥 } ) ) = ( 𝑅 ∩ ( 𝐵 × { 𝐴 } ) ) )
15 14 neeq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑅 ∩ ( 𝐵 × { 𝑥 } ) ) ≠ ∅ ↔ ( 𝑅 ∩ ( 𝐵 × { 𝐴 } ) ) ≠ ∅ ) )
16 elin ⊢ ( 𝑝 ∈ ( 𝑅 ∩ ( 𝐵 × { 𝑥 } ) ) ↔ ( 𝑝 ∈ 𝑅 ∧ 𝑝 ∈ ( 𝐵 × { 𝑥 } ) ) )
17 ancom ⊢ ( ( 𝑝 ∈ 𝑅 ∧ 𝑝 ∈ ( 𝐵 × { 𝑥 } ) ) ↔ ( 𝑝 ∈ ( 𝐵 × { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) )
18 elxp ⊢ ( 𝑝 ∈ ( 𝐵 × { 𝑥 } ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) )
19 18 anbi1i ⊢ ( ( 𝑝 ∈ ( 𝐵 × { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) ↔ ( ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑅 ) )
20 16 17 19 3bitri ⊢ ( 𝑝 ∈ ( 𝑅 ∩ ( 𝐵 × { 𝑥 } ) ) ↔ ( ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑅 ) )
21 20 exbii ⊢ ( ∃ 𝑝 𝑝 ∈ ( 𝑅 ∩ ( 𝐵 × { 𝑥 } ) ) ↔ ∃ 𝑝 ( ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑅 ) )
22 anass ⊢ ( ( ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑅 ) ↔ ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) ) )
23 22 2exbii ⊢ ( ∃ 𝑦 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑅 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) ) )
24 19.41vv ⊢ ( ∃ 𝑦 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑅 ) ↔ ( ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑅 ) )
25 23 24 bitr3i ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) ) ↔ ( ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑅 ) )
26 25 exbii ⊢ ( ∃ 𝑝 ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) ) ↔ ∃ 𝑝 ( ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑅 ) )
27 exrot3 ⊢ ( ∃ 𝑝 ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) ) ↔ ∃ 𝑦 ∃ 𝑧 ∃ 𝑝 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) ) )
28 26 27 bitr3i ⊢ ( ∃ 𝑝 ( ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑅 ) ↔ ∃ 𝑦 ∃ 𝑧 ∃ 𝑝 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) ) )
29 opex ⊢ ⟨ 𝑦 , 𝑧 ⟩ ∈ V
30 eleq1 ⊢ ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑝 ∈ 𝑅 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) )
31 30 anbi2d ⊢ ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) ) )
32 29 31 ceqsexv ⊢ ( ∃ 𝑝 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) )
33 32 exbii ⊢ ( ∃ 𝑧 ∃ 𝑝 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) ) ↔ ∃ 𝑧 ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) )
34 anass ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑧 ∈ { 𝑥 } ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) ) )
35 an12 ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑧 ∈ { 𝑥 } ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) ) ↔ ( 𝑧 ∈ { 𝑥 } ∧ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) ) )
36 velsn ⊢ ( 𝑧 ∈ { 𝑥 } ↔ 𝑧 = 𝑥 )
37 36 anbi1i ⊢ ( ( 𝑧 ∈ { 𝑥 } ∧ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) ) ↔ ( 𝑧 = 𝑥 ∧ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) ) )
38 34 35 37 3bitri ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) ↔ ( 𝑧 = 𝑥 ∧ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) ) )
39 38 exbii ⊢ ( ∃ 𝑧 ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) ) )
40 vex ⊢ 𝑥 ∈ V
41 opeq2 ⊢ ( 𝑧 = 𝑥 → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑦 , 𝑥 ⟩ )
42 41 eleq1d ⊢ ( 𝑧 = 𝑥 → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
43 42 anbi2d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) ) )
44 40 43 ceqsexv ⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
45 33 39 44 3bitri ⊢ ( ∃ 𝑧 ∃ 𝑝 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
46 45 exbii ⊢ ( ∃ 𝑦 ∃ 𝑧 ∃ 𝑝 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ∧ 𝑝 ∈ 𝑅 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
47 21 28 46 3bitri ⊢ ( ∃ 𝑝 𝑝 ∈ ( 𝑅 ∩ ( 𝐵 × { 𝑥 } ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
48 n0 ⊢ ( ( 𝑅 ∩ ( 𝐵 × { 𝑥 } ) ) ≠ ∅ ↔ ∃ 𝑝 𝑝 ∈ ( 𝑅 ∩ ( 𝐵 × { 𝑥 } ) ) )
49 40 elima3 ⊢ ( 𝑥 ∈ ( 𝑅 “ 𝐵 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
50 47 48 49 3bitr4ri ⊢ ( 𝑥 ∈ ( 𝑅 “ 𝐵 ) ↔ ( 𝑅 ∩ ( 𝐵 × { 𝑥 } ) ) ≠ ∅ )
51 11 15 50 vtoclbg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ ( 𝑅 “ 𝐵 ) ↔ ( 𝑅 ∩ ( 𝐵 × { 𝐴 } ) ) ≠ ∅ ) )
52 1 10 51 pm5.21nii ⊢ ( 𝐴 ∈ ( 𝑅 “ 𝐵 ) ↔ ( 𝑅 ∩ ( 𝐵 × { 𝐴 } ) ) ≠ ∅ )