Theorem asymref2 3447

Description: Two ways of saying a relation is antisymmetric and reflexive.

Assertion

Ref	Expression
asymref2	⊢ ((R ∩ ◡R) = (I ↾ ∪∪R) ↔ (∀x ∈ ∪∪RxRx ⋀ ∀x∀y((xRy ⋀ yRx) → x = y)))

Distinct variable group:   x,y,R

Proof of Theorem asymref2

Step	Hyp	Ref	Expression
1		df-ral 1652	. . 3 ⊢ (∀x ∈ ∪∪R∀y((xRy ⋀ yRx) ↔ x = y) ↔ ∀x(x ∈ ∪∪R → ∀y((xRy ⋀ yRx) ↔ x = y)))
2		breq2 2629	. . . . . . . . . . . . 13 ⊢ (y = x → (xRy ↔ xRx))
3		breq1 2628	. . . . . . . . . . . . 13 ⊢ (y = x → (yRx ↔ xRx))
4	2, 3	anbi12d 630	. . . . . . . . . . . 12 ⊢ (y = x → ((xRy ⋀ yRx) ↔ (xRx ⋀ xRx)))
5		anidm 434	. . . . . . . . . . . 12 ⊢ ((xRx ⋀ xRx) ↔ xRx)
6	4, 5	syl6bb 538	. . . . . . . . . . 11 ⊢ (y = x → ((xRy ⋀ yRx) ↔ xRx))
7		equequ2 1137	. . . . . . . . . . 11 ⊢ (y = x → (x = y ↔ x = x))
8	6, 7	bibi12d 631	. . . . . . . . . 10 ⊢ (y = x → (((xRy ⋀ yRx) ↔ x = y) ↔ (xRx ↔ x = x)))
9		equid 1128	. . . . . . . . . . 11 ⊢ x = x
10	9	tbt 722	. . . . . . . . . 10 ⊢ (xRx ↔ (xRx ↔ x = x))
11	8, 10	syl6bbr 540	. . . . . . . . 9 ⊢ (y = x → (((xRy ⋀ yRx) ↔ x = y) ↔ xRx))
12	11	a4v 1274	. . . . . . . 8 ⊢ (∀y((xRy ⋀ yRx) ↔ x = y) → xRx)
13		bi1 148	. . . . . . . . 9 ⊢ (((xRy ⋀ yRx) ↔ x = y) → ((xRy ⋀ yRx) → x = y))
14	13	19.20i 994	. . . . . . . 8 ⊢ (∀y((xRy ⋀ yRx) ↔ x = y) → ∀y((xRy ⋀ yRx) → x = y))
15	12, 14	jca 288	. . . . . . 7 ⊢ (∀y((xRy ⋀ yRx) ↔ x = y) → (xRx ⋀ ∀y((xRy ⋀ yRx) → x = y)))
16		bi3 150	. . . . . . . . . 10 ⊢ (((xRy ⋀ yRx) → x = y) → ((x = y → (xRy ⋀ yRx)) → ((xRy ⋀ yRx) ↔ x = y)))
17		breq2 2629	. . . . . . . . . . . 12 ⊢ (x = y → (xRx ↔ xRy))
18	17	biimpcd 155	. . . . . . . . . . 11 ⊢ (xRx → (x = y → xRy))
19		breq1 2628	. . . . . . . . . . . 12 ⊢ (x = y → (xRx ↔ yRx))
20	19	biimpcd 155	. . . . . . . . . . 11 ⊢ (xRx → (x = y → yRx))
21	18, 20	jcad 602	. . . . . . . . . 10 ⊢ (xRx → (x = y → (xRy ⋀ yRx)))
22	16, 21	syl5com 52	. . . . . . . . 9 ⊢ (xRx → (((xRy ⋀ yRx) → x = y) → ((xRy ⋀ yRx) ↔ x = y)))
23	22	19.20dv 1291	. . . . . . . 8 ⊢ (xRx → (∀y((xRy ⋀ yRx) → x = y) → ∀y((xRy ⋀ yRx) ↔ x = y)))
24	23	imp 350	. . . . . . 7 ⊢ ((xRx ⋀ ∀y((xRy ⋀ yRx) → x = y)) → ∀y((xRy ⋀ yRx) ↔ x = y))
25	15, 24	impbi 157	. . . . . 6 ⊢ (∀y((xRy ⋀ yRx) ↔ x = y) ↔ (xRx ⋀ ∀y((xRy ⋀ yRx) → x = y)))
26	25	imbi2i 185	. . . . 5 ⊢ ((x ∈ ∪∪R → ∀y((xRy ⋀ yRx) ↔ x = y)) ↔ (x ∈ ∪∪R → (xRx ⋀ ∀y((xRy ⋀ yRx) → x = y))))
27		pm4.76 601	. . . . 5 ⊢ (((x ∈ ∪∪R → xRx) ⋀ (x ∈ ∪∪R → ∀y((xRy ⋀ yRx) → x = y))) ↔ (x ∈ ∪∪R → (xRx ⋀ ∀y((xRy ⋀ yRx) → x = y))))
28		visset 1816	. . . . . . . . . . . . . 14 ⊢ x ∈ V
29	28	breldm 3322	. . . . . . . . . . . . 13 ⊢ (xRy → x ∈ dom R)
30		ssun1 2197	. . . . . . . . . . . . . . 15 ⊢ dom R ⊆ (dom R ∪ ran R)
31		dmrnssfld 3364	. . . . . . . . . . . . . . 15 ⊢ (dom R ∪ ran R) ⊆ ∪∪R
32	30, 31	sstri 2077	. . . . . . . . . . . . . 14 ⊢ dom R ⊆ ∪∪R
33	32	sseli 2069	. . . . . . . . . . . . 13 ⊢ (x ∈ dom R → x ∈ ∪∪R)
34	29, 33	syl 10	. . . . . . . . . . . 12 ⊢ (xRy → x ∈ ∪∪R)
35	34	adantr 391	. . . . . . . . . . 11 ⊢ ((xRy ⋀ yRx) → x ∈ ∪∪R)
36	35	pm4.71ri 640	. . . . . . . . . 10 ⊢ ((xRy ⋀ yRx) ↔ (x ∈ ∪∪R ⋀ (xRy ⋀ yRx)))
37	36	imbi1i 186	. . . . . . . . 9 ⊢ (((xRy ⋀ yRx) → x = y) ↔ ((x ∈ ∪∪R ⋀ (xRy ⋀ yRx)) → x = y))
38		impexp 347	. . . . . . . . 9 ⊢ (((x ∈ ∪∪R ⋀ (xRy ⋀ yRx)) → x = y) ↔ (x ∈ ∪∪R → ((xRy ⋀ yRx) → x = y)))
39	37, 38	bitr 173	. . . . . . . 8 ⊢ (((xRy ⋀ yRx) → x = y) ↔ (x ∈ ∪∪R → ((xRy ⋀ yRx) → x = y)))
40	39	albii 1001	. . . . . . 7 ⊢ (∀y((xRy ⋀ yRx) → x = y) ↔ ∀y(x ∈ ∪∪R → ((xRy ⋀ yRx) → x = y)))
41		19.21v 1287	. . . . . . 7 ⊢ (∀y(x ∈ ∪∪R → ((xRy ⋀ yRx) → x = y)) ↔ (x ∈ ∪∪R → ∀y((xRy ⋀ yRx) → x = y)))
42	40, 41	bitr2 174	. . . . . 6 ⊢ ((x ∈ ∪∪R → ∀y((xRy ⋀ yRx) → x = y)) ↔ ∀y((xRy ⋀ yRx) → x = y))
43	42	anbi2i 482	. . . . 5 ⊢ (((x ∈ ∪∪R → xRx) ⋀ (x ∈ ∪∪R → ∀y((xRy ⋀ yRx) → x = y))) ↔ ((x ∈ ∪∪R → xRx) ⋀ ∀y((xRy ⋀ yRx) → x = y)))
44	26, 27, 43	3bitr2 179	. . . 4 ⊢ ((x ∈ ∪∪R → ∀y((xRy ⋀ yRx) ↔ x = y)) ↔ ((x ∈ ∪∪R → xRx) ⋀ ∀y((xRy ⋀ yRx) → x = y)))
45	44	albii 1001	. . 3 ⊢ (∀x(x ∈ ∪∪R → ∀y((xRy ⋀ yRx) ↔ x = y)) ↔ ∀x((x ∈ ∪∪R → xRx) ⋀ ∀y((xRy ⋀ yRx) → x = y)))
46		19.26 1069	. . 3 ⊢ (∀x((x ∈ ∪∪R → xRx) ⋀ ∀y((xRy ⋀ yRx) → x = y)) ↔ (∀x(x ∈ ∪∪R → xRx) ⋀ ∀x∀y((xRy ⋀ yRx) → x = y)))
47	1, 45, 46	3bitr 177	. 2 ⊢ (∀x ∈ ∪∪R∀y((xRy ⋀ yRx) ↔ x = y) ↔ (∀x(x ∈ ∪∪R → xRx) ⋀ ∀x∀y((xRy ⋀ yRx) → x = y)))
48		asymref 3446	. 2 ⊢ ((R ∩ ◡R) = (I ↾ ∪∪R) ↔ ∀x ∈ ∪∪R∀y((xRy ⋀ yRx) ↔ x = y))
49		df-ral 1652	. . 3 ⊢ (∀x ∈ ∪∪RxRx ↔ ∀x(x ∈ ∪∪R → xRx))
50	49	anbi1i 483	. 2 ⊢ ((∀x ∈ ∪∪RxRx ⋀ ∀x∀y((xRy ⋀ yRx) → x = y)) ↔ (∀x(x ∈ ∪∪R → xRx) ⋀ ∀x∀y((xRy ⋀ yRx) → x = y)))
51	47, 48, 50	3bitr4 183	1 ⊢ ((R ∩ ◡R) = (I ↾ ∪∪R) ↔ (∀x ∈ ∪∪RxRx ⋀ ∀x∀y((xRy ⋀ yRx) → x = y)))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 956   = wceq 958   ∈ wcel 960  ∀wral 1648   ∪ cun 2049   ∩ cin 2050  ∪cuni 2508   class class class wbr 2625  Icid 2838  ^◡ccnv 3176  dom cdm 3177  ran crn 3178   ↾ cres 3179

This theorem is referenced by:  pslem 8650

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2709  ax-pow 2749  ax-pr 2786

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-v 1815  df-dif 2053  df-un 2054  df-in 2055  df-ss 2057  df-nul 2285  df-pw 2407  df-sn 2417  df-pr 2418  df-op 2421  df-uni 2509  df-br 2626  df-opab 2673  df-id 2842  df-xp 3191  df-rel 3192  df-cnv 3193  df-dm 3195  df-rn 3196  df-res 3197

Copyright terms: Public domain