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 ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )