Metamath Proof Explorer

Theorem elrnmpores

Description: Membership in the range of a restricted operation class abstraction. (Contributed by Thierry Arnoux, 25-May-2019)

Ref Expression
Hypothesis rngop.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion elrnmpores ( 𝐷 ∈ 𝑉 → ( 𝐷 ∈ ran ( 𝐹 ↾ 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 rngop.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2 eqeq1 ⊢ ( 𝑧 = 𝐷 → ( 𝑧 = 𝐶 ↔ 𝐷 = 𝐶 ) )
3 2 anbi1d ⊢ ( 𝑧 = 𝐷 → ( ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ↔ ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) )
4 3 anbi2d ⊢ ( 𝑧 = 𝐷 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) )
5 4 2exbidv ⊢ ( 𝑧 = 𝐷 → ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) )
6 an12 ⊢ ( ( 𝑝 ∈ 𝑅 ∧ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) ↔ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑝 ∈ 𝑅 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) )
7 an12 ⊢ ( ( 𝑝 ∈ 𝑅 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝑅 ∧ 𝑧 = 𝐶 ) ) )
8 ancom ⊢ ( ( 𝑧 = 𝐶 ∧ 𝑝 ∈ 𝑅 ) ↔ ( 𝑝 ∈ 𝑅 ∧ 𝑧 = 𝐶 ) )
9 eleq1 ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
10 df-br ⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
11 9 10 bitr4di ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 ∈ 𝑅 ↔ 𝑥 𝑅 𝑦 ) )
12 11 anbi2d ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑧 = 𝐶 ∧ 𝑝 ∈ 𝑅 ) ↔ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) )
13 8 12 bitr3id ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑝 ∈ 𝑅 ∧ 𝑧 = 𝐶 ) ↔ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) )
14 13 anbi2d ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝑅 ∧ 𝑧 = 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) )
15 7 14 syl5bb ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑝 ∈ 𝑅 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) )
16 15 pm5.32i ⊢ ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑝 ∈ 𝑅 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) ↔ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) )
17 6 16 bitri ⊢ ( ( 𝑝 ∈ 𝑅 ∧ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) ↔ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) )
18 17 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑝 ∈ 𝑅 ∧ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) )
19 19.42vv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑝 ∈ 𝑅 ∧ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) ↔ ( 𝑝 ∈ 𝑅 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) )
20 18 19 bitr3i ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) ↔ ( 𝑝 ∈ 𝑅 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) )
21 20 opabbii ⊢ { ⟨ 𝑝 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) } = { ⟨ 𝑝 , 𝑧 ⟩ ∣ ( 𝑝 ∈ 𝑅 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) }
22 dfoprab2 ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) } = { ⟨ 𝑝 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) }
23 df-mpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
24 dfoprab2 ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } = { ⟨ 𝑝 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) }
25 1 23 24 3eqtri ⊢ 𝐹 = { ⟨ 𝑝 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) }
26 25 reseq1i ⊢ ( 𝐹 ↾ 𝑅 ) = ( { ⟨ 𝑝 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } ↾ 𝑅 )
27 resopab ⊢ ( { ⟨ 𝑝 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } ↾ 𝑅 ) = { ⟨ 𝑝 , 𝑧 ⟩ ∣ ( 𝑝 ∈ 𝑅 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) }
28 26 27 eqtri ⊢ ( 𝐹 ↾ 𝑅 ) = { ⟨ 𝑝 , 𝑧 ⟩ ∣ ( 𝑝 ∈ 𝑅 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) }
29 21 22 28 3eqtr4ri ⊢ ( 𝐹 ↾ 𝑅 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) }
30 29 rneqi ⊢ ran ( 𝐹 ↾ 𝑅 ) = ran { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) }
31 rnoprab ⊢ ran { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) }
32 30 31 eqtri ⊢ ran ( 𝐹 ↾ 𝑅 ) = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) }
33 5 32 elab2g ⊢ ( 𝐷 ∈ 𝑉 → ( 𝐷 ∈ ran ( 𝐹 ↾ 𝑅 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) )
34 r2ex ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) )
35 33 34 bitr4di ⊢ ( 𝐷 ∈ 𝑉 → ( 𝐷 ∈ ran ( 𝐹 ↾ 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) )