Theorem spwpr2 8658

Description: Property of supremum defining condition for an unordered pair.

Hypothesis

Ref	Expression
spwmo.1	⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy)))

Assertion

Ref	Expression
spwpr2	⊢ (((R ∈ T ⋀ A = {B, C}) ⋀ (B ∈ U ⋀ C ∈ W)) → (φ ↔ ((BRx ⋀ CRx) ⋀ ∀y ∈ X ((BRy ⋀ CRy) → xRy))))

Distinct variable groups:   x,y,z,A   y,B,z   y,C,z   x,R,y,z   x,X,y   y,U   y,W

Proof of Theorem spwpr2

Step	Hyp	Ref	Expression
1		raleq1 1786	. . . . 5 ⊢ (A = {B, C} → (∀y ∈ A yRx ↔ ∀y ∈ {B, C}yRx))
2		ax-17 971	. . . . . . . 8 ⊢ (BRx → ∀y BRx)
3		breq1 2622	. . . . . . . 8 ⊢ (y = B → (yRx ↔ BRx))
4	2, 3	ceqsalg 1825	. . . . . . 7 ⊢ (B ∈ U → (∀y(y = B → yRx) ↔ BRx))
5		ax-17 971	. . . . . . . 8 ⊢ (CRx → ∀y CRx)
6		breq1 2622	. . . . . . . 8 ⊢ (y = C → (yRx ↔ CRx))
7	5, 6	ceqsalg 1825	. . . . . . 7 ⊢ (C ∈ W → (∀y(y = C → yRx) ↔ CRx))
8	4, 7	bi2anan9 632	. . . . . 6 ⊢ ((B ∈ U ⋀ C ∈ W) → ((∀y(y = B → yRx) ⋀ ∀y(y = C → yRx)) ↔ (BRx ⋀ CRx)))
9		df-ral 1649	. . . . . . 7 ⊢ (∀y ∈ {B, C}yRx ↔ ∀y(y ∈ {B, C} → yRx))
10		visset 1813	. . . . . . . . . . 11 ⊢ y ∈ V
11	10	elpr 2424	. . . . . . . . . 10 ⊢ (y ∈ {B, C} ↔ (y = B ⋁ y = C))
12	11	imbi1i 186	. . . . . . . . 9 ⊢ ((y ∈ {B, C} → yRx) ↔ ((y = B ⋁ y = C) → yRx))
13		jaob 422	. . . . . . . . 9 ⊢ (((y = B ⋁ y = C) → yRx) ↔ ((y = B → yRx) ⋀ (y = C → yRx)))
14	12, 13	bitr 173	. . . . . . . 8 ⊢ ((y ∈ {B, C} → yRx) ↔ ((y = B → yRx) ⋀ (y = C → yRx)))
15	14	albii 999	. . . . . . 7 ⊢ (∀y(y ∈ {B, C} → yRx) ↔ ∀y((y = B → yRx) ⋀ (y = C → yRx)))
16		19.26 1067	. . . . . . 7 ⊢ (∀y((y = B → yRx) ⋀ (y = C → yRx)) ↔ (∀y(y = B → yRx) ⋀ ∀y(y = C → yRx)))
17	9, 15, 16	3bitr 177	. . . . . 6 ⊢ (∀y ∈ {B, C}yRx ↔ (∀y(y = B → yRx) ⋀ ∀y(y = C → yRx)))
18	8, 17	syl5bb 532	. . . . 5 ⊢ ((B ∈ U ⋀ C ∈ W) → (∀y ∈ {B, C}yRx ↔ (BRx ⋀ CRx)))
19	1, 18	sylan9bb 540	. . . 4 ⊢ ((A = {B, C} ⋀ (B ∈ U ⋀ C ∈ W)) → (∀y ∈ A yRx ↔ (BRx ⋀ CRx)))
20		raleq1 1786	. . . . . . 7 ⊢ (A = {B, C} → (∀z ∈ A zRy ↔ ∀z ∈ {B, C}zRy))
21		ax-17 971	. . . . . . . . . 10 ⊢ (BRy → ∀z BRy)
22		breq1 2622	. . . . . . . . . 10 ⊢ (z = B → (zRy ↔ BRy))
23	21, 22	ceqsalg 1825	. . . . . . . . 9 ⊢ (B ∈ U → (∀z(z = B → zRy) ↔ BRy))
24		ax-17 971	. . . . . . . . . 10 ⊢ (CRy → ∀z CRy)
25		breq1 2622	. . . . . . . . . 10 ⊢ (z = C → (zRy ↔ CRy))
26	24, 25	ceqsalg 1825	. . . . . . . . 9 ⊢ (C ∈ W → (∀z(z = C → zRy) ↔ CRy))
27	23, 26	bi2anan9 632	. . . . . . . 8 ⊢ ((B ∈ U ⋀ C ∈ W) → ((∀z(z = B → zRy) ⋀ ∀z(z = C → zRy)) ↔ (BRy ⋀ CRy)))
28		df-ral 1649	. . . . . . . . 9 ⊢ (∀z ∈ {B, C}zRy ↔ ∀z(z ∈ {B, C} → zRy))
29		visset 1813	. . . . . . . . . . . . 13 ⊢ z ∈ V
30	29	elpr 2424	. . . . . . . . . . . 12 ⊢ (z ∈ {B, C} ↔ (z = B ⋁ z = C))
31	30	imbi1i 186	. . . . . . . . . . 11 ⊢ ((z ∈ {B, C} → zRy) ↔ ((z = B ⋁ z = C) → zRy))
32		jaob 422	. . . . . . . . . . 11 ⊢ (((z = B ⋁ z = C) → zRy) ↔ ((z = B → zRy) ⋀ (z = C → zRy)))
33	31, 32	bitr 173	. . . . . . . . . 10 ⊢ ((z ∈ {B, C} → zRy) ↔ ((z = B → zRy) ⋀ (z = C → zRy)))
34	33	albii 999	. . . . . . . . 9 ⊢ (∀z(z ∈ {B, C} → zRy) ↔ ∀z((z = B → zRy) ⋀ (z = C → zRy)))
35		19.26 1067	. . . . . . . . 9 ⊢ (∀z((z = B → zRy) ⋀ (z = C → zRy)) ↔ (∀z(z = B → zRy) ⋀ ∀z(z = C → zRy)))
36	28, 34, 35	3bitr 177	. . . . . . . 8 ⊢ (∀z ∈ {B, C}zRy ↔ (∀z(z = B → zRy) ⋀ ∀z(z = C → zRy)))
37	27, 36	syl5bb 532	. . . . . . 7 ⊢ ((B ∈ U ⋀ C ∈ W) → (∀z ∈ {B, C}zRy ↔ (BRy ⋀ CRy)))
38	20, 37	sylan9bb 540	. . . . . 6 ⊢ ((A = {B, C} ⋀ (B ∈ U ⋀ C ∈ W)) → (∀z ∈ A zRy ↔ (BRy ⋀ CRy)))
39	38	imbi1d 613	. . . . 5 ⊢ ((A = {B, C} ⋀ (B ∈ U ⋀ C ∈ W)) → ((∀z ∈ A zRy → xRy) ↔ ((BRy ⋀ CRy) → xRy)))
40	39	ralbidv 1663	. . . 4 ⊢ ((A = {B, C} ⋀ (B ∈ U ⋀ C ∈ W)) → (∀y ∈ X (∀z ∈ A zRy → xRy) ↔ ∀y ∈ X ((BRy ⋀ CRy) → xRy)))
41	19, 40	anbi12d 628	. . 3 ⊢ ((A = {B, C} ⋀ (B ∈ U ⋀ C ∈ W)) → ((∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy)) ↔ ((BRx ⋀ CRx) ⋀ ∀y ∈ X ((BRy ⋀ CRy) → xRy))))
42	41	adantll 392	. 2 ⊢ (((R ∈ T ⋀ A = {B, C}) ⋀ (B ∈ U ⋀ C ∈ W)) → ((∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy)) ↔ ((BRx ⋀ CRx) ⋀ ∀y ∈ X ((BRy ⋀ CRy) → xRy))))
43		spwmo.1	. 2 ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy)))
44	42, 43	syl5bb 532	1 ⊢ (((R ∈ T ⋀ A = {B, C}) ⋀ (B ∈ U ⋀ C ∈ W)) → (φ ↔ ((BRx ⋀ CRx) ⋀ ∀y ∈ X ((BRy ⋀ CRy) → xRy))))

Syntax hints:   → wi 3   ↔ wb 146   ⋁ wo 222   ⋀ wa 223  ∀wal 954   = wceq 956   ∈ wcel 958  ∀wral 1645  {cpr 2410   class class class wbr 2619

This theorem is referenced by:  spwpr3OLD 8662  spwpr4OLD 8663  spwpr4aOLD 8664

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1649  df-v 1812  df-un 2050  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620

Copyright terms: Public domain