Theorem suppsr2 5203

Description: A non-empty, bounded set of positive signed reals has a supremum. (Converts quantifier restrictions to all reals.)

Assertion

Ref	Expression
suppsr2	⊢ (((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ ∃x(x ∈ R ⋀ ∀y(y ∈ R → (y ∈ A → y <R x)))) → ∃x(x ∈ R ⋀ ∀y(y ∈ R → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(z ∈ R ⋀ (z ∈ A ⋀ y <R z)))))))

Distinct variable group:   x,y,z,A

Proof of Theorem suppsr2

Step	Hyp	Ref	Expression
1		hba1 1001	. . . . . 6 ⊢ (∀x(x ∈ A → 0R <R x) → ∀x∀x(x ∈ A → 0R <R x))
2		ax-17 969	. . . . . 6 ⊢ (¬ A = ∅ → ∀x ¬ A = ∅)
3	1, 2	hban 1007	. . . . 5 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → ∀x(∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅))
4		eleq1 1531	. . . . . . . . . . . . . . . 16 ⊢ (x = z → (x ∈ A ↔ z ∈ A))
5		breq2 2618	. . . . . . . . . . . . . . . 16 ⊢ (x = z → (0R <R x ↔ 0R <R z))
6	4, 5	imbi12d 625	. . . . . . . . . . . . . . 15 ⊢ (x = z → ((x ∈ A → 0R <R x) ↔ (z ∈ A → 0R <R z)))
7	6	a4v 1270	. . . . . . . . . . . . . 14 ⊢ (∀x(x ∈ A → 0R <R x) → (z ∈ A → 0R <R z))
8		eleq1 1531	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = z → (y ∈ R ↔ z ∈ R))
9		eleq1 1531	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = z → (y ∈ A ↔ z ∈ A))
10		breq1 2617	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = z → (y <R x ↔ z <R x))
11	9, 10	imbi12d 625	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = z → ((y ∈ A → y <R x) ↔ (z ∈ A → z <R x)))
12	8, 11	imbi12d 625	. . . . . . . . . . . . . . . . . 18 ⊢ (y = z → ((y ∈ R → (y ∈ A → y <R x)) ↔ (z ∈ R → (z ∈ A → z <R x))))
13	12	a4v 1270	. . . . . . . . . . . . . . . . 17 ⊢ (∀y(y ∈ R → (y ∈ A → y <R x)) → (z ∈ R → (z ∈ A → z <R x)))
14		visset 1809	. . . . . . . . . . . . . . . . . . 19 ⊢ z ∈ V
15		ltrelsr 5160	. . . . . . . . . . . . . . . . . . 19 ⊢ <R ⊆ (R × R)
16	14, 15	brel 3218	. . . . . . . . . . . . . . . . . 18 ⊢ (0R <R z → (0R ∈ R ⋀ z ∈ R))
17	16	pm3.27d 325	. . . . . . . . . . . . . . . . 17 ⊢ (0R <R z → z ∈ R)
18	13, 17	syl5 21	. . . . . . . . . . . . . . . 16 ⊢ (∀y(y ∈ R → (y ∈ A → y <R x)) → (0R <R z → (z ∈ A → z <R x)))
19		anc2l 300	. . . . . . . . . . . . . . . 16 ⊢ ((0R <R z → (z ∈ A → z <R x)) → (0R <R z → (z ∈ A → (0R <R z ⋀ z <R x))))
20	18, 19	syl 10	. . . . . . . . . . . . . . 15 ⊢ (∀y(y ∈ R → (y ∈ A → y <R x)) → (0R <R z → (z ∈ A → (0R <R z ⋀ z <R x))))
21		0r 5169	. . . . . . . . . . . . . . . . 17 ⊢ 0R ∈ R
22	21	elisseti 1814	. . . . . . . . . . . . . . . 16 ⊢ 0R ∈ V
23		ltsosr 5183	. . . . . . . . . . . . . . . 16 ⊢ <R Or R
24		visset 1809	. . . . . . . . . . . . . . . 16 ⊢ x ∈ V
25	22, 23, 15, 14, 24	sotri 3435	. . . . . . . . . . . . . . 15 ⊢ ((0R <R z ⋀ z <R x) → 0R <R x)
26	20, 25	syl8 24	. . . . . . . . . . . . . 14 ⊢ (∀y(y ∈ R → (y ∈ A → y <R x)) → (0R <R z → (z ∈ A → 0R <R x)))
27	7, 26	sylan9 468	. . . . . . . . . . . . 13 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ∀y(y ∈ R → (y ∈ A → y <R x))) → (z ∈ A → (z ∈ A → 0R <R x)))
28	27	pm2.43d 65	. . . . . . . . . . . 12 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ∀y(y ∈ R → (y ∈ A → y <R x))) → (z ∈ A → 0R <R x))
29	28	19.23adv 1212	. . . . . . . . . . 11 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ∀y(y ∈ R → (y ∈ A → y <R x))) → (∃z z ∈ A → 0R <R x))
30		n0 2285	. . . . . . . . . . 11 ⊢ (¬ A = ∅ ↔ ∃z z ∈ A)
31	29, 30	syl5ib 206	. . . . . . . . . 10 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ∀y(y ∈ R → (y ∈ A → y <R x))) → (¬ A = ∅ → 0R <R x))
32	31	ex 373	. . . . . . . . 9 ⊢ (∀x(x ∈ A → 0R <R x) → (∀y(y ∈ R → (y ∈ A → y <R x)) → (¬ A = ∅ → 0R <R x)))
33	32	com23 32	. . . . . . . 8 ⊢ (∀x(x ∈ A → 0R <R x) → (¬ A = ∅ → (∀y(y ∈ R → (y ∈ A → y <R x)) → 0R <R x)))
34	33	imp 350	. . . . . . 7 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → (∀y(y ∈ R → (y ∈ A → y <R x)) → 0R <R x))
35		visset 1809	. . . . . . . . . . . 12 ⊢ y ∈ V
36	35, 15	brel 3218	. . . . . . . . . . 11 ⊢ (0R <R y → (0R ∈ R ⋀ y ∈ R))
37	36	pm3.27d 325	. . . . . . . . . 10 ⊢ (0R <R y → y ∈ R)
38	37	imim1i 16	. . . . . . . . 9 ⊢ ((y ∈ R → (y ∈ A → y <R x)) → (0R <R y → (y ∈ A → y <R x)))
39	38	19.20i 990	. . . . . . . 8 ⊢ (∀y(y ∈ R → (y ∈ A → y <R x)) → ∀y(0R <R y → (y ∈ A → y <R x)))
40	39	a1i 8	. . . . . . 7 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → (∀y(y ∈ R → (y ∈ A → y <R x)) → ∀y(0R <R y → (y ∈ A → y <R x))))
41	34, 40	jcad 599	. . . . . 6 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → (∀y(y ∈ R → (y ∈ A → y <R x)) → (0R <R x ⋀ ∀y(0R <R y → (y ∈ A → y <R x)))))
42	41	adantld 390	. . . . 5 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → ((x ∈ R ⋀ ∀y(y ∈ R → (y ∈ A → y <R x))) → (0R <R x ⋀ ∀y(0R <R y → (y ∈ A → y <R x)))))
43	3, 42	19.22d 1060	. . . 4 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → (∃x(x ∈ R ⋀ ∀y(y ∈ R → (y ∈ A → y <R x))) → ∃x(0R <R x ⋀ ∀y(0R <R y → (y ∈ A → y <R x)))))
44	43	imdistani 443	. . 3 ⊢ (((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ ∃x(x ∈ R ⋀ ∀y(y ∈ R → (y ∈ A → y <R x)))) → ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ ∃x(0R <R x ⋀ ∀y(0R <R y → (y ∈ A → y <R x)))))
45		opreq1 3959	. . . . . . 7 ⊢ (v = w → (v +P 1P) = (w +P 1P))
46		opeq1 2483	. . . . . . 7 ⊢ ((v +P 1P) = (w +P 1P) → ⟨(v +P 1P), 1P⟩ = ⟨(w +P 1P), 1P⟩)
47		eceq2 4268	. . . . . . 7 ⊢ (⟨(v +P 1P), 1P⟩ = ⟨(w +P 1P), 1P⟩ → [⟨(v +P 1P), 1P⟩] ~R = [⟨(w +P 1P), 1P⟩] ~R )
48	45, 46, 47	3syl 20	. . . . . 6 ⊢ (v = w → [⟨(v +P 1P), 1P⟩] ~R = [⟨(w +P 1P), 1P⟩] ~R )
49	48	eleq1d 1537	. . . . 5 ⊢ (v = w → ([⟨(v +P 1P), 1P⟩] ~R ∈ A ↔ [⟨(w +P 1P), 1P⟩] ~R ∈ A))
50	49	cbvabv 1905	. . . 4 ⊢ {v∣[⟨(v +P 1P), 1P⟩] ~R ∈ A} = {w∣[⟨(w +P 1P), 1P⟩] ~R ∈ A}
51	50	suppsr 5202	. . 3 ⊢ (((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ ∃x(0R <R x ⋀ ∀y(0R <R y → (y ∈ A → y <R x)))) → ∃x(0R <R x ⋀ ∀y(0R <R y → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z)))))))
52	44, 51	syl 10	. 2 ⊢ (((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ ∃x(x ∈ R ⋀ ∀y(y ∈ R → (y ∈ A → y <R x)))) → ∃x(0R <R x ⋀ ∀y(0R <R y → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z)))))))
53	24, 15	brel 3218	. . . . . . 7 ⊢ (0R <R x → (0R ∈ R ⋀ x ∈ R))
54	53	pm3.27d 325	. . . . . 6 ⊢ (0R <R x → x ∈ R)
55	54	a1i 8	. . . . 5 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → (0R <R x → x ∈ R))
56		eleq1 1531	. . . . . . . . . . . 12 ⊢ (x = y → (x ∈ A ↔ y ∈ A))
57		breq2 2618	. . . . . . . . . . . 12 ⊢ (x = y → (0R <R x ↔ 0R <R y))
58	56, 57	imbi12d 625	. . . . . . . . . . 11 ⊢ (x = y → ((x ∈ A → 0R <R x) ↔ (y ∈ A → 0R <R y)))
59	58	a4v 1270	. . . . . . . . . 10 ⊢ (∀x(x ∈ A → 0R <R x) → (y ∈ A → 0R <R y))
60		imim1 15	. . . . . . . . . . 11 ⊢ ((y ∈ A → 0R <R y) → ((0R <R y → (y ∈ A → ¬ x <R y)) → (y ∈ A → (y ∈ A → ¬ x <R y))))
61		merlem10 932	. . . . . . . . . . 11 ⊢ ((y ∈ A → (y ∈ A → ¬ x <R y)) → (y ∈ R → (y ∈ A → ¬ x <R y)))
62	60, 61	syl6 22	. . . . . . . . . 10 ⊢ ((y ∈ A → 0R <R y) → ((0R <R y → (y ∈ A → ¬ x <R y)) → (y ∈ R → (y ∈ A → ¬ x <R y))))
63	59, 62	syl 10	. . . . . . . . 9 ⊢ (∀x(x ∈ A → 0R <R x) → ((0R <R y → (y ∈ A → ¬ x <R y)) → (y ∈ R → (y ∈ A → ¬ x <R y))))
64	63	adantr 389	. . . . . . . 8 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → ((0R <R y → (y ∈ A → ¬ x <R y)) → (y ∈ R → (y ∈ A → ¬ x <R y))))
65		pm3.27 323	. . . . . . . . . . . 12 ⊢ ((((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ y ∈ R) ⋀ (0R <R y → (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))) → (0R <R y → (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z)))))
66	7	ancld 298	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀x(x ∈ A → 0R <R x) → (z ∈ A → (z ∈ A ⋀ 0R <R z)))
67		sotric 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (( <R Or R ⋀ (0R ∈ R ⋀ y ∈ R)) → (0R <R y ↔ ¬ (0R = y ⋁ y <R 0R)))
68	23, 67	mpan 694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0R ∈ R ⋀ y ∈ R) → (0R <R y ↔ ¬ (0R = y ⋁ y <R 0R)))
69	21, 68	mpan 694	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (y ∈ R → (0R <R y ↔ ¬ (0R = y ⋁ y <R 0R)))
70	69	con2bid 525	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (y ∈ R → ((0R = y ⋁ y <R 0R) ↔ ¬ 0R <R y))
71		breq1 2617	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0R = y → (0R <R z ↔ y <R z))
72	71	biimpd 153	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0R = y → (0R <R z → y <R z))
73	35, 23, 15, 22, 14	sotri 3435	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((y <R 0R ⋀ 0R <R z) → y <R z)
74	73	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (y <R 0R → (0R <R z → y <R z))
75	72, 74	jaoi 341	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0R = y ⋁ y <R 0R) → (0R <R z → y <R z))
76	70, 75	syl6bir 215	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (y ∈ R → (¬ 0R <R y → (0R <R z → y <R z)))
77	76	impcom 351	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 0R <R y ⋀ y ∈ R) → (0R <R z → y <R z))
78	77	ancld 298	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ 0R <R y ⋀ y ∈ R) → (0R <R z → (0R <R z ⋀ y <R z)))
79	78	anim2d 560	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 0R <R y ⋀ y ∈ R) → ((z ∈ A ⋀ 0R <R z) → (z ∈ A ⋀ (0R <R z ⋀ y <R z))))
80		an12 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((z ∈ A ⋀ (0R <R z ⋀ y <R z)) ↔ (0R <R z ⋀ (z ∈ A ⋀ y <R z)))
81	79, 80	syl6ib 212	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 0R <R y ⋀ y ∈ R) → ((z ∈ A ⋀ 0R <R z) → (0R <R z ⋀ (z ∈ A ⋀ y <R z))))
82	66, 81	sylan9 468	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ (¬ 0R <R y ⋀ y ∈ R)) → (z ∈ A → (0R <R z ⋀ (z ∈ A ⋀ y <R z))))
83	82	19.22dv 1288	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ (¬ 0R <R y ⋀ y ∈ R)) → (∃z z ∈ A → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))
84	83, 30	syl5ib 206	. . . . . . . . . . . . . . . . 17 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ (¬ 0R <R y ⋀ y ∈ R)) → (¬ A = ∅ → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))
85	84	exp32 377	. . . . . . . . . . . . . . . 16 ⊢ (∀x(x ∈ A → 0R <R x) → (¬ 0R <R y → (y ∈ R → (¬ A = ∅ → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))))
86	85	com24 37	. . . . . . . . . . . . . . 15 ⊢ (∀x(x ∈ A → 0R <R x) → (¬ A = ∅ → (y ∈ R → (¬ 0R <R y → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))))
87	86	imp31 362	. . . . . . . . . . . . . 14 ⊢ (((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ y ∈ R) → (¬ 0R <R y → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))
88	87	a1dd 42	. . . . . . . . . . . . 13 ⊢ (((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ y ∈ R) → (¬ 0R <R y → (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z)))))
89	88	adantr 389	. . . . . . . . . . . 12 ⊢ ((((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ y ∈ R) ⋀ (0R <R y → (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))) → (¬ 0R <R y → (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z)))))
90	65, 89	pm2.61d 127	. . . . . . . . . . 11 ⊢ ((((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ y ∈ R) ⋀ (0R <R y → (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))) → (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))
91	90	an1rs 489	. . . . . . . . . 10 ⊢ ((((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ (0R <R y → (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))) ⋀ y ∈ R) → (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))
92	17	anim1i 334	. . . . . . . . . . 11 ⊢ ((0R <R z ⋀ (z ∈ A ⋀ y <R z)) → (z ∈ R ⋀ (z ∈ A ⋀ y <R z)))
93	92	19.22i 1038	. . . . . . . . . 10 ⊢ (∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z)) → ∃z(z ∈ R ⋀ (z ∈ A ⋀ y <R z)))
94	91, 93	syl6 22	. . . . . . . . 9 ⊢ ((((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ (0R <R y → (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))) ⋀ y ∈ R) → (y <R x → ∃z(z ∈ R ⋀ (z ∈ A ⋀ y <R z))))
95	94	exp31 376	. . . . . . . 8 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → ((0R <R y → (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z)))) → (y ∈ R → (y <R x → ∃z(z ∈ R ⋀ (z ∈ A ⋀ y <R z))))))
96	64, 95	anim12d 557	. . . . . . 7 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → (((0R <R y → (y ∈ A → ¬ x <R y)) ⋀ (0R <R y → (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))) → ((y ∈ R → (y ∈ A → ¬ x <R y)) ⋀ (y ∈ R → (y <R x → ∃z(z ∈ R ⋀ (z ∈ A ⋀ y <R z)))))))
97		jcab 597	. . . . . . 7 ⊢ ((0R <R y → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))) ↔ ((0R <R y → (y ∈ A → ¬ x <R y)) ⋀ (0R <R y → (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))))
98		jcab 597	. . . . . . 7 ⊢ ((y ∈ R → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(z ∈ R ⋀ (z ∈ A ⋀ y <R z))))) ↔ ((y ∈ R → (y ∈ A → ¬ x <R y)) ⋀ (y ∈ R → (y <R x → ∃z(z ∈ R ⋀ (z ∈ A ⋀ y <R z))))))
99	96, 97, 98	3imtr4g 552	. . . . . 6 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → ((0R <R y → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))) → (y ∈ R → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(z ∈ R ⋀ (z ∈ A ⋀ y <R z)))))))
100	99	19.20dv 1287	. . . . 5 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → (∀y(0R <R y → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z))))) → ∀y(y ∈ R → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(z ∈ R ⋀ (z ∈ A ⋀ y <R z)))))))
101	55, 100	anim12d 557	. . . 4 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → ((0R <R x ⋀ ∀y(0R <R y → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z)))))) → (x ∈ R ⋀ ∀y(y ∈ R → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(z ∈ R ⋀ (z ∈ A ⋀ y <R z))))))))
102	3, 101	19.22d 1060	. . 3 ⊢ ((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) → (∃x(0R <R x ⋀ ∀y(0R <R y → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z)))))) → ∃x(x ∈ R ⋀ ∀y(y ∈ R → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(z ∈ R ⋀ (z ∈ A ⋀ y <R z))))))))
103	102	adantr 389	. 2 ⊢ (((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ ∃x(x ∈ R ⋀ ∀y(y ∈ R → (y ∈ A → y <R x)))) → (∃x(0R <R x ⋀ ∀y(0R <R y → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(0R <R z ⋀ (z ∈ A ⋀ y <R z)))))) → ∃x(x ∈ R ⋀ ∀y(y ∈ R → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(z ∈ R ⋀ (z ∈ A ⋀ y <R z))))))))
104	52, 103	mpd 26	1 ⊢ (((∀x(x ∈ A → 0R <R x) ⋀ ¬ A = ∅) ⋀ ∃x(x ∈ R ⋀ ∀y(y ∈ R → (y ∈ A → y <R x)))) → ∃x(x ∈ R ⋀ ∀y(y ∈ R → ((y ∈ A → ¬ x <R y) ⋀ (y <R x → ∃z(z ∈ R ⋀ (z ∈ A ⋀ y <R z)))))))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋁ wo 222   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  {cab 1461  ∅c0 2276  ⟨cop 2407   class class class wbr 2614   Or wor 2834  (class class class)co 3954  [cec 4249  1_Pc1p 4966   +_P cpp 4967   ~_R cer 4972  Rcnr 4973  0_Rc0r 4974   <_R cltr 4979

This theorem is referenced by:  suppsr3 5204

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861  ax-inf2 4605

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-reu 1648  df-rab 1649  df-v 1808  df-sbc 1938  df-csb 1998  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-pss 2051  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2499  df-int 2529  df-iun 2563  df-br 2615  df-opab 2662  df-tr 2676  df-eprel 2827  df-id 2830  df-po 2835  df-so 2845  df-fr 2912  df-we 2929  df-ord 2946  df-on 2947  df-lim 2948  df-suc 2949  df-om 3127  df-xp 3179  df-rel 3180  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fun 3187  df-fn 3188  df-f 3189  df-fv 3193  df-rdg 3923  df-opr 3956  df-oprab 3957  df-1st 4069  df-2nd 4070  df-1o 4123  df-oadd 4125  df-omul 4126  df-er 4251  df-ec 4253  df-qs 4256  df-ni 4980  df-pli 4981  df-mi 4982  df-lti 4983  df-plpq 5015  df-mpq 5016  df-enq 5017  df-nq 5018  df-plq 5019  df-mq 5020  df-rq 5021  df-ltq 5022  df-1q 5023  df-np 5066  df-1p 5067  df-plp 5068  df-ltp 5070  df-enr 5146  df-nr 5147  df-ltr 5150  df-0r 5151

Copyright terms: Public domain