Theorem relop 4409

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 4275	. 2 ⊢ (Rel ⟨A, B⟩ ↔ ⟨A, B⟩ ⊆ (V × V))
2		dfss2 2907	. . . . 5 ⊢ (⟨A, B⟩ ⊆ (V × V) ↔ ∀z(z ∈ ⟨A, B⟩ → z ∈ (V × V)))
3		vex 2534	. . . . . . . . . 10 ⊢ z ∈ V
4		relop.1	. . . . . . . . . 10 ⊢ A ∈ V
5		relop.2	. . . . . . . . . 10 ⊢ B ∈ V
6	3, 4, 5	elop 3938	. . . . . . . . 9 ⊢ (z ∈ ⟨A, B⟩ ↔ (z = {A} ∨ z = {A, B}))
7		elvv 4325	. . . . . . . . 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 618	. . . . . . . 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 1335	. . . . . 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 1346	. . . . . 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 3905	. . . . . . . 8 ⊢ (A ∈ V → {A} ∈ V)
16	4, 15	ax-mp 7	. . . . . . 7 ⊢ {A} ∈ V
17		eqeq1 2024	. . . . . . . 8 ⊢ (z = {A} → (z = {A} ↔ {A} = {A}))
18		eqeq1 2024	. . . . . . . . . 10 ⊢ (z = {A} → (z = ⟨x, y⟩ ↔ {A} = ⟨x, y⟩))
19		eqcom 2020	. . . . . . . . . . 11 ⊢ ({A} = ⟨x, y⟩ ↔ ⟨x, y⟩ = {A})
20		vex 2534	. . . . . . . . . . . 12 ⊢ x ∈ V
21		vex 2534	. . . . . . . . . . . 12 ⊢ y ∈ V
22	20, 21, 4	opeqsn 3959	. . . . . . . . . . 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 1726	. . . . . . . 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 2619	. . . . . 6 ⊢ (∀z(z = {A} → ∃x∃y z = ⟨x, y⟩) → ({A} = {A} → ∃x∃y(x = y ∧ A = {x})))
28		sneq 3357	. . . . . . . . 9 ⊢ (w = x → {w} = {x})
29	28	eqeq2d 2029	. . . . . . . 8 ⊢ (w = x → (A = {w} ↔ A = {x}))
30	29	cbvexv 1773	. . . . . . 7 ⊢ (∃w A = {w} ↔ ∃x A = {x})
31		a9ev 1565	. . . . . . . . . 10 ⊢ ∃y y = x
32		equcom 1571	. . . . . . . . . . 11 ⊢ (y = x ↔ x = y)
33	32	exbii 1474	. . . . . . . . . 10 ⊢ (∃y y = x ↔ ∃y x = y)
34	31, 33	mpbi 133	. . . . . . . . 9 ⊢ ∃y x = y
35		19.41v 1760	. . . . . . . . 9 ⊢ (∃y(x = y ∧ A = {x}) ↔ (∃y x = y ∧ A = {x}))
36	34, 35	mpbiran 833	. . . . . . . 8 ⊢ (∃y(x = y ∧ A = {x}) ↔ A = {x})
37	36	exbii 1474	. . . . . . 7 ⊢ (∃x∃y(x = y ∧ A = {x}) ↔ ∃x A = {x})
38		eqid 2018	. . . . . . . 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 2018	. . . . . 6 ⊢ {A, B} = {A, B}
43		prexgOLD 3916	. . . . . . . 8 ⊢ ((A ∈ V ∧ B ∈ V) → {A, B} ∈ V)
44	4, 5, 43	mp2an 404	. . . . . . 7 ⊢ {A, B} ∈ V
45		eqeq1 2024	. . . . . . . 8 ⊢ (z = {A, B} → (z = {A, B} ↔ {A, B} = {A, B}))
46		eqeq1 2024	. . . . . . . . 9 ⊢ (z = {A, B} → (z = ⟨x, y⟩ ↔ {A, B} = ⟨x, y⟩))
47	46	2exbidv 1726	. . . . . . . 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 2619	. . . . . 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 2020	. . . . . . . . . 10 ⊢ ({A, B} = ⟨x, y⟩ ↔ ⟨x, y⟩ = {A, B})
52	20, 21, 4, 5	opeqpr 3960	. . . . . . . . . 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 2036	. . . . . . . . . . . . . 14 ⊢ ((A = {x, y} ∧ A = {w}) → {x, y} = {w})
56		vex 2534	. . . . . . . . . . . . . . . 16 ⊢ w ∈ V
57	20, 21, 56	preqsn 3516	. . . . . . . . . . . . . . 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 3360	. . . . . . . . . . . . . . . . . . . 20 ⊢ {x} = {x, x}
61		preq2 3418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = y → {x, x} = {x, y})
62	60, 61	syl5req 2063	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = y → {x, y} = {x})
63	62	eqeq2d 2029	. . . . . . . . . . . . . . . . . 18 ⊢ (x = y → (A = {x, y} ↔ A = {x}))
64	60, 61	syl5eq 2062	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = y → {x} = {x, y})
65	64	eqeq2d 2029	. . . . . . . . . . . . . . . . . 18 ⊢ (x = y → (B = {x} ↔ B = {x, y}))
66	63, 65	anbi12d 445	. . . . . . . . . . . . . . . . 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 624	. . . . . . . . 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 1740	. . . . . . 7 ⊢ (A = {w} → (∃x∃y{A, B} = ⟨x, y⟩ → ∃x∃y(A = {x} ∧ B = {x, y})))
77	76	exlimiv 1467	. . . . . 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 1567	. . . . . . . . . . . . . 14 ⊢ x = x
83	82	jctl 297	. . . . . . . . . . . . 13 ⊢ (A = {x} → (x = x ∧ A = {x}))
84	20, 20, 4	opeqsn 3959	. . . . . . . . . . . . 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 2053	. . . . . . . . . 10 ⊢ ((A = {x} ∧ z = {A}) → z = ⟨x, x⟩)
88		opeq12 3521	. . . . . . . . . . . 12 ⊢ ((w = x ∧ v = x) → ⟨w, v⟩ = ⟨x, x⟩)
89	88	eqeq2d 2029	. . . . . . . . . . 11 ⊢ ((w = x ∧ v = x) → (z = ⟨w, v⟩ ↔ z = ⟨x, x⟩))
90	20, 20, 89	spc2ev 2621	. . . . . . . . . 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 449	. . . . . . . 8 ⊢ (((A = {x} ∧ B = {x, y}) ∧ z = {A}) → ∃w∃v z = ⟨w, v⟩)
93		preq12 3419	. . . . . . . . . . . 12 ⊢ ((A = {x} ∧ B = {x, y}) → {A, B} = {{x}, {x, y}})
94	93	eqeq2d 2029	. . . . . . . . . . 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 3518	. . . . . . . . . 10 ⊢ ⟨x, y⟩ = {{x}, {x, y}}
97	95, 96	syl6eqr 2068	. . . . . . . . 9 ⊢ (((A = {x} ∧ B = {x, y}) ∧ z = {A, B}) → z = ⟨x, y⟩)
98		opeq12 3521	. . . . . . . . . . 11 ⊢ ((w = x ∧ v = y) → ⟨w, v⟩ = ⟨x, y⟩)
99	98	eqeq2d 2029	. . . . . . . . . 10 ⊢ ((w = x ∧ v = y) → (z = ⟨w, v⟩ ↔ z = ⟨x, y⟩))
100	20, 21, 99	spc2ev 2621	. . . . . . . . 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 697	. . . . . . 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 4325	. . . . . 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 2924	. . . 4 ⊢ ((A = {x} ∧ B = {x, y}) → ⟨A, B⟩ ⊆ (V × V))
107	106	exlimivv 1754	. . 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 616  ∀wal 1224   = wceq 1226  ∃wex 1358   ∈ wcel 1370  Vcvv 2531   ⊆ wss 2890  {csn 3346  {cpr 3347  ⟨cop 3349   × cxp 4266  Rel wrel 4273

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 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-v 2533  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-opab 3789  df-xp 4274  df-rel 4275

This theorem is referenced by:  funopg  4856