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	⊢ ( 𝐴 ∈ ( 𝑅 “ 𝐵 ) ↔ ( 𝑅 ∩ ( 𝐵 × { 𝐴 } ) ) ≠ ∅ )