Metamath Proof Explorer

Theorem poprelb

Description: Equality for unordered pairs with partially ordered elements. (Contributed by AV, 9-Jul-2023)

Ref Expression
Assertion poprelb ( ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
2 an3 ⊢ ( ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) ) → ( Rel 𝑅 ∧ 𝐶 𝑅 𝐷 ) )
3 2 3adant2 ⊢ ( ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) ) → ( Rel 𝑅 ∧ 𝐶 𝑅 𝐷 ) )
4 brrelex12 ⊢ ( ( Rel 𝑅 ∧ 𝐶 𝑅 𝐷 ) → ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) )
5 3 4 syl ⊢ ( ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) ) → ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) )
6 preq12bg ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
7 1 5 6 syl2anc ⊢ ( ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
8 idd ⊢ ( ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
9 breq12 ⊢ ( ( 𝐵 = 𝐶 ∧ 𝐴 = 𝐷 ) → ( 𝐵 𝑅 𝐴 ↔ 𝐶 𝑅 𝐷 ) )
10 9 ancoms ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐵 𝑅 𝐴 ↔ 𝐶 𝑅 𝐷 ) )
11 10 bicomd ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐶 𝑅 𝐷 ↔ 𝐵 𝑅 𝐴 ) )
12 11 anbi2d ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) ↔ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) ) )
13 po2nr ⊢ ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ¬ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) )
14 13 adantll ⊢ ( ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ¬ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) )
15 14 pm2.21d ⊢ ( ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
16 15 ex ⊢ ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) )
17 16 com13 ⊢ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) )
18 12 17 biimtrdi ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) ) )
19 18 com23 ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) → ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) ) )
20 19 com14 ⊢ ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) → ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) ) )
21 20 3imp ⊢ ( ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) ) → ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
22 8 21 jaod ⊢ ( ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) ) → ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
23 orc ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) )
24 22 23 impbid1 ⊢ ( ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) ) → ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
25 7 24 bitrd ⊢ ( ( ( Rel 𝑅 ∧ 𝑅 Po 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )