Theorem opkthg 4132

Description: Two Kuratowski ordered pairs are equal iff their components are equal. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
opkthg	|- ((A e. V /\ B e. W /\ D e. T) -> (<<A, B>> = <<C, D>> <-> (A = C /\ B = D)))

Proof of Theorem opkthg

Step	Hyp	Ref	Expression
1		simp1 955	. . . . 5 |- ((A e. V /\ B e. W /\ D e. T) -> A e. V)
2		opkth1g 4131	. . . . 5 |- ((A e. V /\ <<A, B>> = <<C, D>>) -> A = C)
3	1, 2	sylan 457	. . . 4 |- (((A e. V /\ B e. W /\ D e. T) /\ <<A, B>> = <<C, D>>) -> A = C)
4		simp2 956	. . . . . 6 |- ((A e. V /\ B e. W /\ D e. T) -> B e. W)
5		simp3 957	. . . . . 6 |- ((A e. V /\ B e. W /\ D e. T) -> D e. T)
6	4, 5	jca 518	. . . . 5 |- ((A e. V /\ B e. W /\ D e. T) -> (B e. W /\ D e. T))
7		opkeq1 4060	. . . . . . . . . . 11 |- (A = C -> <<A, B>> = <<C, B>>)
8	7	eqeq1d 2361	. . . . . . . . . 10 |- (A = C -> (<<A, B>> = <<C, D>> <-> <<C, B>> = <<C, D>>))
9	8	biimpd 198	. . . . . . . . 9 |- (A = C -> (<<A, B>> = <<C, D>> -> <<C, B>> = <<C, D>>))
10	9	impcom 419	. . . . . . . 8 |- ((<<A, B>> = <<C, D>> /\ A = C) -> <<C, B>> = <<C, D>>)
11		df-opk 4059	. . . . . . . . . . 11 |- <<C, B>> = {{C}, {C, B}}
12		df-opk 4059	. . . . . . . . . . 11 |- <<C, D>> = {{C}, {C, D}}
13	11, 12	eqeq12i 2366	. . . . . . . . . 10 |- (<<C, B>> = <<C, D>> <-> {{C}, {C, B}} = {{C}, {C, D}})
14		prex 4113	. . . . . . . . . . 11 |- {C, B} e. _V
15		prex 4113	. . . . . . . . . . 11 |- {C, D} e. _V
16	14, 15	preqr2 4126	. . . . . . . . . 10 |- ({{C}, {C, B}} = {{C}, {C, D}} -> {C, B} = {C, D})
17	13, 16	sylbi 187	. . . . . . . . 9 |- (<<C, B>> = <<C, D>> -> {C, B} = {C, D})
18		preqr2g 4127	. . . . . . . . 9 |- ((B e. W /\ D e. T) -> ({C, B} = {C, D} -> B = D))
19	17, 18	syl5 28	. . . . . . . 8 |- ((B e. W /\ D e. T) -> (<<C, B>> = <<C, D>> -> B = D))
20	10, 19	syl5 28	. . . . . . 7 |- ((B e. W /\ D e. T) -> ((<<A, B>> = <<C, D>> /\ A = C) -> B = D))
21	20	exp3a 425	. . . . . 6 |- ((B e. W /\ D e. T) -> (<<A, B>> = <<C, D>> -> (A = C -> B = D)))
22	21	imp 418	. . . . 5 |- (((B e. W /\ D e. T) /\ <<A, B>> = <<C, D>>) -> (A = C -> B = D))
23	6, 22	sylan 457	. . . 4 |- (((A e. V /\ B e. W /\ D e. T) /\ <<A, B>> = <<C, D>>) -> (A = C -> B = D))
24	3, 23	jcai 522	. . 3 |- (((A e. V /\ B e. W /\ D e. T) /\ <<A, B>> = <<C, D>>) -> (A = C /\ B = D))
25	24	ex 423	. 2 |- ((A e. V /\ B e. W /\ D e. T) -> (<<A, B>> = <<C, D>> -> (A = C /\ B = D)))
26		opkeq12 4062	. 2 |- ((A = C /\ B = D) -> <<A, B>> = <<C, D>>)
27	25, 26	impbid1 194	1 |- ((A e. V /\ B e. W /\ D e. T) -> (<<A, B>> = <<C, D>> <-> (A = C /\ B = D)))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358   /\ w3a 934   = wceq 1642   e. wcel 1710  {csn 3738  {cpr 3739  <<copk 4058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-ss 3260  df-nul 3552  df-sn 3742  df-pr 3743  df-opk 4059

This theorem is referenced by:  opkth  4133  opkelopkabg  4246  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262