Metamath Proof Explorer


Theorem opeldifid

Description: Ordered pair elementhood outside of the diagonal. (Contributed by Thierry Arnoux, 1-Jan-2020)

Ref Expression
Assertion opeldifid ( Rel 𝐴 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 ∖ I ) ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝐴𝑋𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 reldif ( Rel 𝐴 → Rel ( 𝐴 ∖ I ) )
2 brrelex2 ( ( Rel ( 𝐴 ∖ I ) ∧ 𝑋 ( 𝐴 ∖ I ) 𝑌 ) → 𝑌 ∈ V )
3 1 2 sylan ( ( Rel 𝐴𝑋 ( 𝐴 ∖ I ) 𝑌 ) → 𝑌 ∈ V )
4 brrelex2 ( ( Rel 𝐴𝑋 𝐴 𝑌 ) → 𝑌 ∈ V )
5 4 adantrr ( ( Rel 𝐴 ∧ ( 𝑋 𝐴 𝑌𝑋𝑌 ) ) → 𝑌 ∈ V )
6 brdif ( 𝑋 ( 𝐴 ∖ I ) 𝑌 ↔ ( 𝑋 𝐴 𝑌 ∧ ¬ 𝑋 I 𝑌 ) )
7 ideqg ( 𝑌 ∈ V → ( 𝑋 I 𝑌𝑋 = 𝑌 ) )
8 7 necon3bbid ( 𝑌 ∈ V → ( ¬ 𝑋 I 𝑌𝑋𝑌 ) )
9 8 anbi2d ( 𝑌 ∈ V → ( ( 𝑋 𝐴 𝑌 ∧ ¬ 𝑋 I 𝑌 ) ↔ ( 𝑋 𝐴 𝑌𝑋𝑌 ) ) )
10 6 9 syl5bb ( 𝑌 ∈ V → ( 𝑋 ( 𝐴 ∖ I ) 𝑌 ↔ ( 𝑋 𝐴 𝑌𝑋𝑌 ) ) )
11 3 5 10 pm5.21nd ( Rel 𝐴 → ( 𝑋 ( 𝐴 ∖ I ) 𝑌 ↔ ( 𝑋 𝐴 𝑌𝑋𝑌 ) ) )
12 df-br ( 𝑋 ( 𝐴 ∖ I ) 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 ∖ I ) )
13 df-br ( 𝑋 𝐴 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝐴 )
14 13 anbi1i ( ( 𝑋 𝐴 𝑌𝑋𝑌 ) ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝐴𝑋𝑌 ) )
15 11 12 14 3bitr3g ( Rel 𝐴 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 ∖ I ) ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝐴𝑋𝑌 ) ) )