Metamath Proof Explorer

Theorem opth

Description: The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of TakeutiZaring p. 16. Note that C and D are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995)

Ref Expression
Hypotheses opth1.1 𝐴 ∈ V
opth1.2 𝐵 ∈ V
Assertion opth ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 opth1.1 𝐴 ∈ V
2 opth1.2 𝐵 ∈ V
3 1 2 opth1 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → 𝐴 = 𝐶 )
4 1 2 opi1 { 𝐴 } ∈ ⟨ 𝐴 , 𝐵
5 id ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
6 4 5 eleqtrid ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ )
7 oprcl ( { 𝐴 } ∈ ⟨ 𝐶 , 𝐷 ⟩ → ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) )
8 6 7 syl ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) )
9 8 simprd ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → 𝐷 ∈ V )
10 3 opeq1d ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐵 ⟩ )
11 10 5 eqtr3d ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ⟨ 𝐶 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
12 8 simpld ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 ∈ V )
13 dfopg ( ( 𝐶 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐶 , 𝐵 ⟩ = { { 𝐶 } , { 𝐶 , 𝐵 } } )
14 12 2 13 sylancl ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ⟨ 𝐶 , 𝐵 ⟩ = { { 𝐶 } , { 𝐶 , 𝐵 } } )
15 11 14 eqtr3d ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ⟨ 𝐶 , 𝐷 ⟩ = { { 𝐶 } , { 𝐶 , 𝐵 } } )
16 dfopg ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ⟨ 𝐶 , 𝐷 ⟩ = { { 𝐶 } , { 𝐶 , 𝐷 } } )
17 8 16 syl ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ⟨ 𝐶 , 𝐷 ⟩ = { { 𝐶 } , { 𝐶 , 𝐷 } } )
18 15 17 eqtr3d ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → { { 𝐶 } , { 𝐶 , 𝐵 } } = { { 𝐶 } , { 𝐶 , 𝐷 } } )
19 prex { 𝐶 , 𝐵 } ∈ V
20 prex { 𝐶 , 𝐷 } ∈ V
21 19 20 preqr2 ( { { 𝐶 } , { 𝐶 , 𝐵 } } = { { 𝐶 } , { 𝐶 , 𝐷 } } → { 𝐶 , 𝐵 } = { 𝐶 , 𝐷 } )
22 18 21 syl ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → { 𝐶 , 𝐵 } = { 𝐶 , 𝐷 } )
23 preq2 ( 𝑥 = 𝐷 → { 𝐶 , 𝑥 } = { 𝐶 , 𝐷 } )
24 23 eqeq2d ( 𝑥 = 𝐷 → ( { 𝐶 , 𝐵 } = { 𝐶 , 𝑥 } ↔ { 𝐶 , 𝐵 } = { 𝐶 , 𝐷 } ) )
25 eqeq2 ( 𝑥 = 𝐷 → ( 𝐵 = 𝑥𝐵 = 𝐷 ) )
26 24 25 imbi12d ( 𝑥 = 𝐷 → ( ( { 𝐶 , 𝐵 } = { 𝐶 , 𝑥 } → 𝐵 = 𝑥 ) ↔ ( { 𝐶 , 𝐵 } = { 𝐶 , 𝐷 } → 𝐵 = 𝐷 ) ) )
27 vex 𝑥 ∈ V
28 2 27 preqr2 ( { 𝐶 , 𝐵 } = { 𝐶 , 𝑥 } → 𝐵 = 𝑥 )
29 26 28 vtoclg ( 𝐷 ∈ V → ( { 𝐶 , 𝐵 } = { 𝐶 , 𝐷 } → 𝐵 = 𝐷 ) )
30 9 22 29 sylc ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → 𝐵 = 𝐷 )
31 3 30 jca ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝐴 = 𝐶𝐵 = 𝐷 ) )
32 opeq12 ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
33 31 32 impbii ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) )