Metamath Proof Explorer

Theorem opbrop

Description: Ordered pair membership in a relation. Special case. (Contributed by NM, 5-Aug-1995)

Ref Expression
Hypotheses opbrop.1 ⊢ ( ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ ( 𝑣 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( 𝜑 ↔ 𝜓 ) )
opbrop.2 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ) }
Assertion opbrop ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝑅 ⟨ 𝐶 , 𝐷 ⟩ ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 opbrop.1 ⊢ ( ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ ( 𝑣 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( 𝜑 ↔ 𝜓 ) )
2 opbrop.2 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ) }
3 opelxpi ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) )
4 opelxpi ⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) )
5 3 4 anim12i ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) ) )
6 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
7 opex ⊢ ⟨ 𝐶 , 𝐷 ⟩ ∈ V
8 eleq1 ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ) )
9 8 anbi1d ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ) )
10 eqeq1 ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ) )
11 10 anbi1d ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ) )
12 11 anbi1d ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ) )
13 12 4exbidv ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ) )
14 9 13 anbi12d ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ) ) )
15 eleq1 ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑦 ∈ ( 𝑆 × 𝑆 ) ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) ) )
16 15 anbi2d ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) ) ) )
17 eqeq1 ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ↔ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑣 , 𝑢 ⟩ ) )
18 17 anbi2d ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑣 , 𝑢 ⟩ ) ) )
19 18 anbi1d ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ) )
20 19 4exbidv ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ) )
21 16 20 anbi12d ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ) ) )
22 6 7 14 21 2 brab ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ 𝑅 ⟨ 𝐶 , 𝐷 ⟩ ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ) )
23 1 copsex4g ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ↔ 𝜓 ) )
24 23 anbi2d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ 𝜑 ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) ) ∧ 𝜓 ) ) )
25 22 24 bitrid ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝑅 ⟨ 𝐶 , 𝐷 ⟩ ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) ) ∧ 𝜓 ) ) )
26 5 25 mpbirand ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝑅 ⟨ 𝐶 , 𝐷 ⟩ ↔ 𝜓 ) )