Metamath Proof Explorer


Theorem elxp5

Description: Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 when the double intersection does not create class existence problems (caused by int0 ). (Contributed by NM, 1-Aug-2004)

Ref Expression
Assertion elxp5 ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 = ⟨ 𝐴 , ran { 𝐴 } ⟩ ∧ ( 𝐴𝐵 ran { 𝐴 } ∈ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 elxp ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐵𝑦𝐶 ) ) )
2 sneq ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → { 𝐴 } = { ⟨ 𝑥 , 𝑦 ⟩ } )
3 2 rneqd ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ran { 𝐴 } = ran { ⟨ 𝑥 , 𝑦 ⟩ } )
4 3 unieqd ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ran { 𝐴 } = ran { ⟨ 𝑥 , 𝑦 ⟩ } )
5 vex 𝑥 ∈ V
6 vex 𝑦 ∈ V
7 5 6 op2nda ran { ⟨ 𝑥 , 𝑦 ⟩ } = 𝑦
8 4 7 eqtr2di ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑦 = ran { 𝐴 } )
9 8 pm4.71ri ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑦 = ran { 𝐴 } ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) )
10 9 anbi1i ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐵𝑦𝐶 ) ) ↔ ( ( 𝑦 = ran { 𝐴 } ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ( 𝑥𝐵𝑦𝐶 ) ) )
11 anass ( ( ( 𝑦 = ran { 𝐴 } ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ( 𝑥𝐵𝑦𝐶 ) ) ↔ ( 𝑦 = ran { 𝐴 } ∧ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐵𝑦𝐶 ) ) ) )
12 10 11 bitri ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐵𝑦𝐶 ) ) ↔ ( 𝑦 = ran { 𝐴 } ∧ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐵𝑦𝐶 ) ) ) )
13 12 exbii ( ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐵𝑦𝐶 ) ) ↔ ∃ 𝑦 ( 𝑦 = ran { 𝐴 } ∧ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐵𝑦𝐶 ) ) ) )
14 snex { 𝐴 } ∈ V
15 14 rnex ran { 𝐴 } ∈ V
16 15 uniex ran { 𝐴 } ∈ V
17 opeq2 ( 𝑦 = ran { 𝐴 } → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , ran { 𝐴 } ⟩ )
18 17 eqeq2d ( 𝑦 = ran { 𝐴 } → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ) )
19 eleq1 ( 𝑦 = ran { 𝐴 } → ( 𝑦𝐶 ran { 𝐴 } ∈ 𝐶 ) )
20 19 anbi2d ( 𝑦 = ran { 𝐴 } → ( ( 𝑥𝐵𝑦𝐶 ) ↔ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) )
21 18 20 anbi12d ( 𝑦 = ran { 𝐴 } → ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐵𝑦𝐶 ) ) ↔ ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) ) )
22 16 21 ceqsexv ( ∃ 𝑦 ( 𝑦 = ran { 𝐴 } ∧ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐵𝑦𝐶 ) ) ) ↔ ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) )
23 13 22 bitri ( ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐵𝑦𝐶 ) ) ↔ ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) )
24 inteq ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ → 𝐴 = 𝑥 , ran { 𝐴 } ⟩ )
25 24 inteqd ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ → 𝐴 = 𝑥 , ran { 𝐴 } ⟩ )
26 5 16 op1stb 𝑥 , ran { 𝐴 } ⟩ = 𝑥
27 25 26 eqtr2di ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ → 𝑥 = 𝐴 )
28 27 pm4.71ri ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ↔ ( 𝑥 = 𝐴𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ) )
29 28 anbi1i ( ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) ↔ ( ( 𝑥 = 𝐴𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ) ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) )
30 anass ( ( ( 𝑥 = 𝐴𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ) ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) ↔ ( 𝑥 = 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) ) )
31 23 29 30 3bitri ( ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐵𝑦𝐶 ) ) ↔ ( 𝑥 = 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) ) )
32 31 exbii ( ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐵𝑦𝐶 ) ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) ) )
33 eqvisset ( 𝑥 = 𝐴 𝐴 ∈ V )
34 33 adantr ( ( 𝑥 = 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) ) → 𝐴 ∈ V )
35 34 exlimiv ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) ) → 𝐴 ∈ V )
36 elex ( 𝐴𝐵 𝐴 ∈ V )
37 36 ad2antrl ( ( 𝐴 = ⟨ 𝐴 , ran { 𝐴 } ⟩ ∧ ( 𝐴𝐵 ran { 𝐴 } ∈ 𝐶 ) ) → 𝐴 ∈ V )
38 opeq1 ( 𝑥 = 𝐴 → ⟨ 𝑥 , ran { 𝐴 } ⟩ = ⟨ 𝐴 , ran { 𝐴 } ⟩ )
39 38 eqeq2d ( 𝑥 = 𝐴 → ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ↔ 𝐴 = ⟨ 𝐴 , ran { 𝐴 } ⟩ ) )
40 eleq1 ( 𝑥 = 𝐴 → ( 𝑥𝐵 𝐴𝐵 ) )
41 40 anbi1d ( 𝑥 = 𝐴 → ( ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ↔ ( 𝐴𝐵 ran { 𝐴 } ∈ 𝐶 ) ) )
42 39 41 anbi12d ( 𝑥 = 𝐴 → ( ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) ↔ ( 𝐴 = ⟨ 𝐴 , ran { 𝐴 } ⟩ ∧ ( 𝐴𝐵 ran { 𝐴 } ∈ 𝐶 ) ) ) )
43 42 ceqsexgv ( 𝐴 ∈ V → ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) ) ↔ ( 𝐴 = ⟨ 𝐴 , ran { 𝐴 } ⟩ ∧ ( 𝐴𝐵 ran { 𝐴 } ∈ 𝐶 ) ) ) )
44 35 37 43 pm5.21nii ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ran { 𝐴 } ⟩ ∧ ( 𝑥𝐵 ran { 𝐴 } ∈ 𝐶 ) ) ) ↔ ( 𝐴 = ⟨ 𝐴 , ran { 𝐴 } ⟩ ∧ ( 𝐴𝐵 ran { 𝐴 } ∈ 𝐶 ) ) )
45 1 32 44 3bitri ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 = ⟨ 𝐴 , ran { 𝐴 } ⟩ ∧ ( 𝐴𝐵 ran { 𝐴 } ∈ 𝐶 ) ) )