Theorem relop 4429

Description: A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.)

Hypotheses

Ref	Expression
relop.1	⊢ A ∈ V
relop.2	⊢ B ∈ V

Assertion

Ref	Expression
relop	⊢ (Rel ⟨A, B⟩ ↔ ∃x∃y(A = {x} ∧ B = {x, y}))

Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem relop

Dummy variables w v z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rel 4295	. 2 ⊢ (Rel ⟨A, B⟩ ↔ ⟨A, B⟩ ⊆ (V × V))
2		dfss2 2928	. . . . 5 ⊢ (⟨A, B⟩ ⊆ (V × V) ↔ ∀z(z ∈ ⟨A, B⟩ → z ∈ (V × V)))
3		vex 2554	. . . . . . . . . 10 ⊢ z ∈ V
4		relop.1	. . . . . . . . . 10 ⊢ A ∈ V
5		relop.2	. . . . . . . . . 10 ⊢ B ∈ V
6	3, 4, 5	elop 3959	. . . . . . . . 9 ⊢ (z ∈ ⟨A, B⟩ ↔ (z = {A} ∨ z = {A, B}))
7		elvv 4345	. . . . . . . . 9 ⊢ (z ∈ (V × V) ↔ ∃x∃y z = ⟨x, y⟩)
8	6, 7	imbi12i 228	. . . . . . . 8 ⊢ ((z ∈ ⟨A, B⟩ → z ∈ (V × V)) ↔ ((z = {A} ∨ z = {A, B}) → ∃x∃y z = ⟨x, y⟩))
9		jaob 630	. . . . . . . 8 ⊢ (((z = {A} ∨ z = {A, B}) → ∃x∃y z = ⟨x, y⟩) ↔ ((z = {A} → ∃x∃y z = ⟨x, y⟩) ∧ (z = {A, B} → ∃x∃y z = ⟨x, y⟩)))
10	8, 9	bitri 173	. . . . . . 7 ⊢ ((z ∈ ⟨A, B⟩ → z ∈ (V × V)) ↔ ((z = {A} → ∃x∃y z = ⟨x, y⟩) ∧ (z = {A, B} → ∃x∃y z = ⟨x, y⟩)))
11	10	albii 1356	. . . . . 6 ⊢ (∀z(z ∈ ⟨A, B⟩ → z ∈ (V × V)) ↔ ∀z((z = {A} → ∃x∃y z = ⟨x, y⟩) ∧ (z = {A, B} → ∃x∃y z = ⟨x, y⟩)))
12		19.26 1367	. . . . . 6 ⊢ (∀z((z = {A} → ∃x∃y z = ⟨x, y⟩) ∧ (z = {A, B} → ∃x∃y z = ⟨x, y⟩)) ↔ (∀z(z = {A} → ∃x∃y z = ⟨x, y⟩) ∧ ∀z(z = {A, B} → ∃x∃y z = ⟨x, y⟩)))
13	11, 12	bitri 173	. . . . 5 ⊢ (∀z(z ∈ ⟨A, B⟩ → z ∈ (V × V)) ↔ (∀z(z = {A} → ∃x∃y z = ⟨x, y⟩) ∧ ∀z(z = {A, B} → ∃x∃y z = ⟨x, y⟩)))
14	2, 13	bitri 173	. . . 4 ⊢ (⟨A, B⟩ ⊆ (V × V) ↔ (∀z(z = {A} → ∃x∃y z = ⟨x, y⟩) ∧ ∀z(z = {A, B} → ∃x∃y z = ⟨x, y⟩)))
15		snexgOLD 3926	. . . . . . . 8 ⊢ (A ∈ V → {A} ∈ V)
16	4, 15	ax-mp 7	. . . . . . 7 ⊢ {A} ∈ V
17		eqeq1 2043	. . . . . . . 8 ⊢ (z = {A} → (z = {A} ↔ {A} = {A}))
18		eqeq1 2043	. . . . . . . . . 10 ⊢ (z = {A} → (z = ⟨x, y⟩ ↔ {A} = ⟨x, y⟩))
19		eqcom 2039	. . . . . . . . . . 11 ⊢ ({A} = ⟨x, y⟩ ↔ ⟨x, y⟩ = {A})
20		vex 2554	. . . . . . . . . . . 12 ⊢ x ∈ V
21		vex 2554	. . . . . . . . . . . 12 ⊢ y ∈ V
22	20, 21, 4	opeqsn 3980	. . . . . . . . . . 11 ⊢ (⟨x, y⟩ = {A} ↔ (x = y ∧ A = {x}))
23	19, 22	bitri 173	. . . . . . . . . 10 ⊢ ({A} = ⟨x, y⟩ ↔ (x = y ∧ A = {x}))
24	18, 23	syl6bb 185	. . . . . . . . 9 ⊢ (z = {A} → (z = ⟨x, y⟩ ↔ (x = y ∧ A = {x})))
25	24	2exbidv 1745	. . . . . . . 8 ⊢ (z = {A} → (∃x∃y z = ⟨x, y⟩ ↔ ∃x∃y(x = y ∧ A = {x})))
26	17, 25	imbi12d 223	. . . . . . 7 ⊢ (z = {A} → ((z = {A} → ∃x∃y z = ⟨x, y⟩) ↔ ({A} = {A} → ∃x∃y(x = y ∧ A = {x}))))
27	16, 26	spcv 2640	. . . . . 6 ⊢ (∀z(z = {A} → ∃x∃y z = ⟨x, y⟩) → ({A} = {A} → ∃x∃y(x = y ∧ A = {x})))
28		sneq 3378	. . . . . . . . 9 ⊢ (w = x → {w} = {x})
29	28	eqeq2d 2048	. . . . . . . 8 ⊢ (w = x → (A = {w} ↔ A = {x}))
30	29	cbvexv 1792	. . . . . . 7 ⊢ (∃w A = {w} ↔ ∃x A = {x})
31		a9ev 1584	. . . . . . . . . 10 ⊢ ∃y y = x
32		equcom 1590	. . . . . . . . . . 11 ⊢ (y = x ↔ x = y)
33	32	exbii 1493	. . . . . . . . . 10 ⊢ (∃y y = x ↔ ∃y x = y)
34	31, 33	mpbi 133	. . . . . . . . 9 ⊢ ∃y x = y
35		19.41v 1779	. . . . . . . . 9 ⊢ (∃y(x = y ∧ A = {x}) ↔ (∃y x = y ∧ A = {x}))
36	34, 35	mpbiran 846	. . . . . . . 8 ⊢ (∃y(x = y ∧ A = {x}) ↔ A = {x})
37	36	exbii 1493	. . . . . . 7 ⊢ (∃x∃y(x = y ∧ A = {x}) ↔ ∃x A = {x})
38		eqid 2037	. . . . . . . 8 ⊢ {A} = {A}
39	38	a1bi 232	. . . . . . 7 ⊢ (∃x∃y(x = y ∧ A = {x}) ↔ ({A} = {A} → ∃x∃y(x = y ∧ A = {x})))
40	30, 37, 39	3bitr2ri 198	. . . . . 6 ⊢ (({A} = {A} → ∃x∃y(x = y ∧ A = {x})) ↔ ∃w A = {w})
41	27, 40	sylib 127	. . . . 5 ⊢ (∀z(z = {A} → ∃x∃y z = ⟨x, y⟩) → ∃w A = {w})
42		eqid 2037	. . . . . 6 ⊢ {A, B} = {A, B}
43		prexgOLD 3937	. . . . . . . 8 ⊢ ((A ∈ V ∧ B ∈ V) → {A, B} ∈ V)
44	4, 5, 43	mp2an 402	. . . . . . 7 ⊢ {A, B} ∈ V
45		eqeq1 2043	. . . . . . . 8 ⊢ (z = {A, B} → (z = {A, B} ↔ {A, B} = {A, B}))
46		eqeq1 2043	. . . . . . . . 9 ⊢ (z = {A, B} → (z = ⟨x, y⟩ ↔ {A, B} = ⟨x, y⟩))
47	46	2exbidv 1745	. . . . . . . 8 ⊢ (z = {A, B} → (∃x∃y z = ⟨x, y⟩ ↔ ∃x∃y{A, B} = ⟨x, y⟩))
48	45, 47	imbi12d 223	. . . . . . 7 ⊢ (z = {A, B} → ((z = {A, B} → ∃x∃y z = ⟨x, y⟩) ↔ ({A, B} = {A, B} → ∃x∃y{A, B} = ⟨x, y⟩)))
49	44, 48	spcv 2640	. . . . . 6 ⊢ (∀z(z = {A, B} → ∃x∃y z = ⟨x, y⟩) → ({A, B} = {A, B} → ∃x∃y{A, B} = ⟨x, y⟩))
50	42, 49	mpi 15	. . . . 5 ⊢ (∀z(z = {A, B} → ∃x∃y z = ⟨x, y⟩) → ∃x∃y{A, B} = ⟨x, y⟩)
51		eqcom 2039	. . . . . . . . . 10 ⊢ ({A, B} = ⟨x, y⟩ ↔ ⟨x, y⟩ = {A, B})
52	20, 21, 4, 5	opeqpr 3981	. . . . . . . . . 10 ⊢ (⟨x, y⟩ = {A, B} ↔ ((A = {x} ∧ B = {x, y}) ∨ (A = {x, y} ∧ B = {x})))
53	51, 52	bitri 173	. . . . . . . . 9 ⊢ ({A, B} = ⟨x, y⟩ ↔ ((A = {x} ∧ B = {x, y}) ∨ (A = {x, y} ∧ B = {x})))
54		idd 21	. . . . . . . . . 10 ⊢ (A = {w} → ((A = {x} ∧ B = {x, y}) → (A = {x} ∧ B = {x, y})))
55		eqtr2 2055	. . . . . . . . . . . . . 14 ⊢ ((A = {x, y} ∧ A = {w}) → {x, y} = {w})
56		vex 2554	. . . . . . . . . . . . . . . 16 ⊢ w ∈ V
57	20, 21, 56	preqsn 3537	. . . . . . . . . . . . . . 15 ⊢ ({x, y} = {w} ↔ (x = y ∧ y = w))
58	57	simplbi 259	. . . . . . . . . . . . . 14 ⊢ ({x, y} = {w} → x = y)
59	55, 58	syl 14	. . . . . . . . . . . . 13 ⊢ ((A = {x, y} ∧ A = {w}) → x = y)
60		dfsn2 3381	. . . . . . . . . . . . . . . . . . . 20 ⊢ {x} = {x, x}
61		preq2 3439	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = y → {x, x} = {x, y})
62	60, 61	syl5req 2082	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = y → {x, y} = {x})
63	62	eqeq2d 2048	. . . . . . . . . . . . . . . . . 18 ⊢ (x = y → (A = {x, y} ↔ A = {x}))
64	60, 61	syl5eq 2081	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = y → {x} = {x, y})
65	64	eqeq2d 2048	. . . . . . . . . . . . . . . . . 18 ⊢ (x = y → (B = {x} ↔ B = {x, y}))
66	63, 65	anbi12d 442	. . . . . . . . . . . . . . . . 17 ⊢ (x = y → ((A = {x, y} ∧ B = {x}) ↔ (A = {x} ∧ B = {x, y})))
67	66	biimpd 132	. . . . . . . . . . . . . . . 16 ⊢ (x = y → ((A = {x, y} ∧ B = {x}) → (A = {x} ∧ B = {x, y})))
68	67	expd 245	. . . . . . . . . . . . . . 15 ⊢ (x = y → (A = {x, y} → (B = {x} → (A = {x} ∧ B = {x, y}))))
69	68	com12 27	. . . . . . . . . . . . . 14 ⊢ (A = {x, y} → (x = y → (B = {x} → (A = {x} ∧ B = {x, y}))))
70	69	adantr 261	. . . . . . . . . . . . 13 ⊢ ((A = {x, y} ∧ A = {w}) → (x = y → (B = {x} → (A = {x} ∧ B = {x, y}))))
71	59, 70	mpd 13	. . . . . . . . . . . 12 ⊢ ((A = {x, y} ∧ A = {w}) → (B = {x} → (A = {x} ∧ B = {x, y})))
72	71	expcom 109	. . . . . . . . . . 11 ⊢ (A = {w} → (A = {x, y} → (B = {x} → (A = {x} ∧ B = {x, y}))))
73	72	impd 242	. . . . . . . . . 10 ⊢ (A = {w} → ((A = {x, y} ∧ B = {x}) → (A = {x} ∧ B = {x, y})))
74	54, 73	jaod 636	. . . . . . . . 9 ⊢ (A = {w} → (((A = {x} ∧ B = {x, y}) ∨ (A = {x, y} ∧ B = {x})) → (A = {x} ∧ B = {x, y})))
75	53, 74	syl5bi 141	. . . . . . . 8 ⊢ (A = {w} → ({A, B} = ⟨x, y⟩ → (A = {x} ∧ B = {x, y})))
76	75	2eximdv 1759	. . . . . . 7 ⊢ (A = {w} → (∃x∃y{A, B} = ⟨x, y⟩ → ∃x∃y(A = {x} ∧ B = {x, y})))
77	76	exlimiv 1486	. . . . . 6 ⊢ (∃w A = {w} → (∃x∃y{A, B} = ⟨x, y⟩ → ∃x∃y(A = {x} ∧ B = {x, y})))
78	77	imp 115	. . . . 5 ⊢ ((∃w A = {w} ∧ ∃x∃y{A, B} = ⟨x, y⟩) → ∃x∃y(A = {x} ∧ B = {x, y}))
79	41, 50, 78	syl2an 273	. . . 4 ⊢ ((∀z(z = {A} → ∃x∃y z = ⟨x, y⟩) ∧ ∀z(z = {A, B} → ∃x∃y z = ⟨x, y⟩)) → ∃x∃y(A = {x} ∧ B = {x, y}))
80	14, 79	sylbi 114	. . 3 ⊢ (⟨A, B⟩ ⊆ (V × V) → ∃x∃y(A = {x} ∧ B = {x, y}))
81		simpr 103	. . . . . . . . . . 11 ⊢ ((A = {x} ∧ z = {A}) → z = {A})
82		equid 1586	. . . . . . . . . . . . . 14 ⊢ x = x
83	82	jctl 297	. . . . . . . . . . . . 13 ⊢ (A = {x} → (x = x ∧ A = {x}))
84	20, 20, 4	opeqsn 3980	. . . . . . . . . . . . 13 ⊢ (⟨x, x⟩ = {A} ↔ (x = x ∧ A = {x}))
85	83, 84	sylibr 137	. . . . . . . . . . . 12 ⊢ (A = {x} → ⟨x, x⟩ = {A})
86	85	adantr 261	. . . . . . . . . . 11 ⊢ ((A = {x} ∧ z = {A}) → ⟨x, x⟩ = {A})
87	81, 86	eqtr4d 2072	. . . . . . . . . 10 ⊢ ((A = {x} ∧ z = {A}) → z = ⟨x, x⟩)
88		opeq12 3542	. . . . . . . . . . . 12 ⊢ ((w = x ∧ v = x) → ⟨w, v⟩ = ⟨x, x⟩)
89	88	eqeq2d 2048	. . . . . . . . . . 11 ⊢ ((w = x ∧ v = x) → (z = ⟨w, v⟩ ↔ z = ⟨x, x⟩))
90	20, 20, 89	spc2ev 2642	. . . . . . . . . 10 ⊢ (z = ⟨x, x⟩ → ∃w∃v z = ⟨w, v⟩)
91	87, 90	syl 14	. . . . . . . . 9 ⊢ ((A = {x} ∧ z = {A}) → ∃w∃v z = ⟨w, v⟩)
92	91	adantlr 446	. . . . . . . 8 ⊢ (((A = {x} ∧ B = {x, y}) ∧ z = {A}) → ∃w∃v z = ⟨w, v⟩)
93		preq12 3440	. . . . . . . . . . . 12 ⊢ ((A = {x} ∧ B = {x, y}) → {A, B} = {{x}, {x, y}})
94	93	eqeq2d 2048	. . . . . . . . . . 11 ⊢ ((A = {x} ∧ B = {x, y}) → (z = {A, B} ↔ z = {{x}, {x, y}}))
95	94	biimpa 280	. . . . . . . . . 10 ⊢ (((A = {x} ∧ B = {x, y}) ∧ z = {A, B}) → z = {{x}, {x, y}})
96	20, 21	dfop 3539	. . . . . . . . . 10 ⊢ ⟨x, y⟩ = {{x}, {x, y}}
97	95, 96	syl6eqr 2087	. . . . . . . . 9 ⊢ (((A = {x} ∧ B = {x, y}) ∧ z = {A, B}) → z = ⟨x, y⟩)
98		opeq12 3542	. . . . . . . . . . 11 ⊢ ((w = x ∧ v = y) → ⟨w, v⟩ = ⟨x, y⟩)
99	98	eqeq2d 2048	. . . . . . . . . 10 ⊢ ((w = x ∧ v = y) → (z = ⟨w, v⟩ ↔ z = ⟨x, y⟩))
100	20, 21, 99	spc2ev 2642	. . . . . . . . 9 ⊢ (z = ⟨x, y⟩ → ∃w∃v z = ⟨w, v⟩)
101	97, 100	syl 14	. . . . . . . 8 ⊢ (((A = {x} ∧ B = {x, y}) ∧ z = {A, B}) → ∃w∃v z = ⟨w, v⟩)
102	92, 101	jaodan 709	. . . . . . 7 ⊢ (((A = {x} ∧ B = {x, y}) ∧ (z = {A} ∨ z = {A, B})) → ∃w∃v z = ⟨w, v⟩)
103	102	ex 108	. . . . . 6 ⊢ ((A = {x} ∧ B = {x, y}) → ((z = {A} ∨ z = {A, B}) → ∃w∃v z = ⟨w, v⟩))
104		elvv 4345	. . . . . 6 ⊢ (z ∈ (V × V) ↔ ∃w∃v z = ⟨w, v⟩)
105	103, 6, 104	3imtr4g 194	. . . . 5 ⊢ ((A = {x} ∧ B = {x, y}) → (z ∈ ⟨A, B⟩ → z ∈ (V × V)))
106	105	ssrdv 2945	. . . 4 ⊢ ((A = {x} ∧ B = {x, y}) → ⟨A, B⟩ ⊆ (V × V))
107	106	exlimivv 1773	. . 3 ⊢ (∃x∃y(A = {x} ∧ B = {x, y}) → ⟨A, B⟩ ⊆ (V × V))
108	80, 107	impbii 117	. 2 ⊢ (⟨A, B⟩ ⊆ (V × V) ↔ ∃x∃y(A = {x} ∧ B = {x, y}))
109	1, 108	bitri 173	1 ⊢ (Rel ⟨A, B⟩ ↔ ∃x∃y(A = {x} ∧ B = {x, y}))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628  ∀wal 1240   = wceq 1242  ∃wex 1378   ∈ wcel 1390  Vcvv 2551   ⊆ wss 2911  {csn 3367  {cpr 3368  ⟨cop 3370   × cxp 4286  Rel wrel 4293

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-opab 3810  df-xp 4294  df-rel 4295

This theorem is referenced by:  funopg  4877