Theorem suppsr3 4018

Description: A non-empty, bounded set with at least one positive real has a supremum.

Hypothesis

Ref	Expression
suppsr3.1	⊢ B = {y∣(y ∈ A ∧ 0R <R y)}

Assertion

Ref	Expression
suppsr3	⊢ ((∃y(y ∈ A ∧ 0R <R y) ∧ ∃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(s):   x,y,z,A   x,B,y,z

Proof of Theorem suppsr3

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . . 7 ⊢ x ∈ V
2		eleq1 1149	. . . . . . . 8 ⊢ (y = x → (y ∈ A ↔ x ∈ A))
3		breq2 2066	. . . . . . . 8 ⊢ (y = x → (0R <R y ↔ 0R <R x))
4	2, 3	anbi12d 476	. . . . . . 7 ⊢ (y = x → ((y ∈ A ∧ 0R <R y) ↔ (x ∈ A ∧ 0R <R x)))
5		suppsr3.1	. . . . . . 7 ⊢ B = {y∣(y ∈ A ∧ 0R <R y)}
6	1, 4, 5	elab2 1419	. . . . . 6 ⊢ (x ∈ B ↔ (x ∈ A ∧ 0R <R x))
7	6	pm3.27bd 263	. . . . 5 ⊢ (x ∈ B → 0R <R x)
8	7	ax-gen 677	. . . 4 ⊢ ∀x(x ∈ B → 0R <R x)
9		suppsr2 4017	. . . 4 ⊢ (((∀x(x ∈ B → 0R <R x) ∧ ¬ B = ∅) ∧ ∃x(x ∈ R ∧ ∀y(y ∈ R → (y ∈ B → y <R x)))) → ∃x(x ∈ R ∧ ∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z)))))))
10	8, 9	mpan11 529	. . 3 ⊢ ((¬ B = ∅ ∧ ∃x(x ∈ R ∧ ∀y(y ∈ R → (y ∈ B → y <R x)))) → ∃x(x ∈ R ∧ ∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z)))))))
11		n0 1714	. . . . 5 ⊢ (¬ B = ∅ ↔ ∃y y ∈ B)
12	5	cleqabi 1176	. . . . . 6 ⊢ (y ∈ B ↔ (y ∈ A ∧ 0R <R y))
13	12	biex 733	. . . . 5 ⊢ (∃y y ∈ B ↔ ∃y(y ∈ A ∧ 0R <R y))
14	11, 13	bitr 151	. . . 4 ⊢ (¬ B = ∅ ↔ ∃y(y ∈ A ∧ 0R <R y))
15	14	biimpr 134	. . 3 ⊢ (∃y(y ∈ A ∧ 0R <R y) → ¬ B = ∅)
16	12	pm3.26bd 259	. . . . . . . 8 ⊢ (y ∈ B → y ∈ A)
17	16	syl4 19	. . . . . . 7 ⊢ ((y ∈ A → y <R x) → (y ∈ B → y <R x))
18	17	syl3 18	. . . . . 6 ⊢ ((y ∈ R → (y ∈ A → y <R x)) → (y ∈ R → (y ∈ B → y <R x)))
19	18	19.20i 691	. . . . 5 ⊢ (∀y(y ∈ R → (y ∈ A → y <R x)) → ∀y(y ∈ R → (y ∈ B → y <R x)))
20	19	anim2i 270	. . . 4 ⊢ ((x ∈ R ∧ ∀y(y ∈ R → (y ∈ A → y <R x))) → (x ∈ R ∧ ∀y(y ∈ R → (y ∈ B → y <R x))))
21	20	19.22i 723	. . 3 ⊢ (∃x(x ∈ R ∧ ∀y(y ∈ R → (y ∈ A → y <R x))) → ∃x(x ∈ R ∧ ∀y(y ∈ R → (y ∈ B → y <R x))))
22	10, 15, 21	syl2an 349	. 2 ⊢ ((∃y(y ∈ A ∧ 0R <R y) ∧ ∃x(x ∈ R ∧ ∀y(y ∈ R → (y ∈ A → y <R x)))) → ∃x(x ∈ R ∧ ∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z)))))))
23		hbe1 709	. . . . . . . . 9 ⊢ (∃y(y ∈ A ∧ 0R <R y) → ∀y∃y(y ∈ A ∧ 0R <R y))
24		ax-17 925	. . . . . . . . 9 ⊢ (x ∈ R → ∀y x ∈ R)
25	23, 24	hban 704	. . . . . . . 8 ⊢ ((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) → ∀y(∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R))
26		hba1 698	. . . . . . . 8 ⊢ (∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))))) → ∀y∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))))))
27	25, 26	hban 704	. . . . . . 7 ⊢ (((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) ∧ ∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z)))))) → ∀y((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) ∧ ∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z)))))))
28	12	imbi1i 161	. . . . . . . . . . . . . . . . . 18 ⊢ ((y ∈ B → ¬ x <R y) ↔ ((y ∈ A ∧ 0R <R y) → ¬ x <R y))
29		impexp 276	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ A ∧ 0R <R y) → ¬ x <R y) ↔ (y ∈ A → (0R <R y → ¬ x <R y)))
30	28, 29	bitr 151	. . . . . . . . . . . . . . . . 17 ⊢ ((y ∈ B → ¬ x <R y) ↔ (y ∈ A → (0R <R y → ¬ x <R y)))
31		pm2.04 31	. . . . . . . . . . . . . . . . 17 ⊢ ((y ∈ A → (0R <R y → ¬ x <R y)) → (0R <R y → (y ∈ A → ¬ x <R y)))
32	30, 31	sylbi 174	. . . . . . . . . . . . . . . 16 ⊢ ((y ∈ B → ¬ x <R y) → (0R <R y → (y ∈ A → ¬ x <R y)))
33	32	syl3 18	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ R → (y ∈ B → ¬ x <R y)) → (y ∈ R → (0R <R y → (y ∈ A → ¬ x <R y))))
34	33	com23 32	. . . . . . . . . . . . . 14 ⊢ ((y ∈ R → (y ∈ B → ¬ x <R y)) → (0R <R y → (y ∈ R → (y ∈ A → ¬ x <R y))))
35	34	a4s 682	. . . . . . . . . . . . 13 ⊢ (∀y(y ∈ R → (y ∈ B → ¬ x <R y)) → (0R <R y → (y ∈ R → (y ∈ A → ¬ x <R y))))
36	35	adantl 305	. . . . . . . . . . . 12 ⊢ (((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) ∧ ∀y(y ∈ R → (y ∈ B → ¬ x <R y))) → (0R <R y → (y ∈ R → (y ∈ A → ¬ x <R y))))
37		hba1 698	. . . . . . . . . . . . . . . . . 18 ⊢ (∀y(y ∈ R → (y ∈ B → ¬ x <R y)) → ∀y∀y(y ∈ R → (y ∈ B → ¬ x <R y)))
38		ax-17 925	. . . . . . . . . . . . . . . . . 18 ⊢ (0R <R x → ∀y0R <R x)
39	37, 38	hbim 702	. . . . . . . . . . . . . . . . 17 ⊢ ((∀y(y ∈ R → (y ∈ B → ¬ x <R y)) → 0R <R x) → ∀y(∀y(y ∈ R → (y ∈ B → ¬ x <R y)) → 0R <R x))
40	24, 39	hbim 702	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ R → (∀y(y ∈ R → (y ∈ B → ¬ x <R y)) → 0R <R x)) → ∀y(x ∈ R → (∀y(y ∈ R → (y ∈ B → ¬ x <R y)) → 0R <R x)))
41		ltsosr 3997	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ <R Or R
42		sotric 2148	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (( <R Or R ∧ (x ∈ R ∧ y ∈ R)) → (x <R y ↔ ¬ (x = y ∨ y <R x)))
43	41, 42	mpan 518	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((x ∈ R ∧ y ∈ R) → (x <R y ↔ ¬ (x = y ∨ y <R x)))
44	43	bicon2d 404	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((x ∈ R ∧ y ∈ R) → ((x = y ∨ y <R x) ↔ ¬ x <R y))
45		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ y ∈ V
46		ltrelsr 3974	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ <R ⊆ (R × R)
47	45, 46	brel 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0R <R y → (0R ∈ R ∧ y ∈ R))
48	47	pm3.27d 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0R <R y → y ∈ R)
49	44, 48	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((x ∈ R ∧ 0R <R y) → ((x = y ∨ y <R x) ↔ ¬ x <R y))
50		breq2 2066	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (x = y → (0R <R x ↔ 0R <R y))
51	50	biimprcd 138	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0R <R y → (x = y → 0R <R x))
52		0r 3983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0R ∈ R
53	52	elisseti 1355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0R ∈ V
54	53, 41, 46, 45, 1	sotri 2630	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0R <R y ∧ y <R x) → 0R <R x)
55	54	exp 291	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0R <R y → (y <R x → 0R <R x))
56	51, 55	jaod 329	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0R <R y → ((x = y ∨ y <R x) → 0R <R x))
57	56	adantl 305	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((x ∈ R ∧ 0R <R y) → ((x = y ∨ y <R x) → 0R <R x))
58	49, 57	sylbird 180	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((x ∈ R ∧ 0R <R y) → (¬ x <R y → 0R <R x))
59	58	exp 291	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (x ∈ R → (0R <R y → (¬ x <R y → 0R <R x)))
60	59	adantld 307	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x ∈ R → ((y ∈ A ∧ 0R <R y) → (¬ x <R y → 0R <R x)))
61	60	a2d 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x ∈ R → (((y ∈ A ∧ 0R <R y) → ¬ x <R y) → ((y ∈ A ∧ 0R <R y) → 0R <R x)))
62	61, 28	syl5ib 181	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x ∈ R → ((y ∈ B → ¬ x <R y) → ((y ∈ A ∧ 0R <R y) → 0R <R x)))
63	62	syl3d 26	. . . . . . . . . . . . . . . . . . 19 ⊢ (x ∈ R → ((y ∈ R → (y ∈ B → ¬ x <R y)) → (y ∈ R → ((y ∈ A ∧ 0R <R y) → 0R <R x))))
64	48	syl4 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ R → ((y ∈ A ∧ 0R <R y) → 0R <R x)) → (0R <R y → ((y ∈ A ∧ 0R <R y) → 0R <R x)))
65		anabs7 376	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0R <R y ∧ (y ∈ A ∧ 0R <R y)) ↔ (y ∈ A ∧ 0R <R y))
66	65	imbi1i 161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((0R <R y ∧ (y ∈ A ∧ 0R <R y)) → 0R <R x) ↔ ((y ∈ A ∧ 0R <R y) → 0R <R x))
67		impexp 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((0R <R y ∧ (y ∈ A ∧ 0R <R y)) → 0R <R x) ↔ (0R <R y → ((y ∈ A ∧ 0R <R y) → 0R <R x)))
68	66, 67	bitr3 153	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((y ∈ A ∧ 0R <R y) → 0R <R x) ↔ (0R <R y → ((y ∈ A ∧ 0R <R y) → 0R <R x)))
69	64, 68	sylibr 175	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ R → ((y ∈ A ∧ 0R <R y) → 0R <R x)) → ((y ∈ A ∧ 0R <R y) → 0R <R x))
70	63, 69	syl6 23	. . . . . . . . . . . . . . . . . 18 ⊢ (x ∈ R → ((y ∈ R → (y ∈ B → ¬ x <R y)) → ((y ∈ A ∧ 0R <R y) → 0R <R x)))
71	70	a4sd 683	. . . . . . . . . . . . . . . . 17 ⊢ (x ∈ R → (∀y(y ∈ R → (y ∈ B → ¬ x <R y)) → ((y ∈ A ∧ 0R <R y) → 0R <R x)))
72	71	com3r 35	. . . . . . . . . . . . . . . 16 ⊢ ((y ∈ A ∧ 0R <R y) → (x ∈ R → (∀y(y ∈ R → (y ∈ B → ¬ x <R y)) → 0R <R x)))
73	40, 72	19.23ai 746	. . . . . . . . . . . . . . 15 ⊢ (∃y(y ∈ A ∧ 0R <R y) → (x ∈ R → (∀y(y ∈ R → (y ∈ B → ¬ x <R y)) → 0R <R x)))
74	73	imp31 280	. . . . . . . . . . . . . 14 ⊢ (((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) ∧ ∀y(y ∈ R → (y ∈ B → ¬ x <R y))) → 0R <R x)
75	53, 41, 46, 1, 45	sotri 2630	. . . . . . . . . . . . . . . 16 ⊢ ((0R <R x ∧ x <R y) → 0R <R y)
76	75	exp 291	. . . . . . . . . . . . . . 15 ⊢ (0R <R x → (x <R y → 0R <R y))
77	76	con3d 87	. . . . . . . . . . . . . 14 ⊢ (0R <R x → (¬ 0R <R y → ¬ x <R y))
78	74, 77	syl 12	. . . . . . . . . . . . 13 ⊢ (((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) ∧ ∀y(y ∈ R → (y ∈ B → ¬ x <R y))) → (¬ 0R <R y → ¬ x <R y))
79		ax-1 3	. . . . . . . . . . . . . 14 ⊢ (¬ x <R y → (y ∈ A → ¬ x <R y))
80	79	a1d 14	. . . . . . . . . . . . 13 ⊢ (¬ x <R y → (y ∈ R → (y ∈ A → ¬ x <R y)))
81	78, 80	syl6 23	. . . . . . . . . . . 12 ⊢ (((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) ∧ ∀y(y ∈ R → (y ∈ B → ¬ x <R y))) → (¬ 0R <R y → (y ∈ R → (y ∈ A → ¬ x <R y))))
82	36, 81	pm2.61d 112	. . . . . . . . . . 11 ⊢ (((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) ∧ ∀y(y ∈ R → (y ∈ B → ¬ x <R y))) → (y ∈ R → (y ∈ A → ¬ x <R y)))
83	82	exp 291	. . . . . . . . . 10 ⊢ ((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) → (∀y(y ∈ R → (y ∈ B → ¬ x <R y)) → (y ∈ R → (y ∈ A → ¬ x <R y))))
84		visset 1350	. . . . . . . . . . . . . . . . . . 19 ⊢ z ∈ V
85		eleq1 1149	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = z → (y ∈ A ↔ z ∈ A))
86		breq2 2066	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = z → (0R <R y ↔ 0R <R z))
87	85, 86	anbi12d 476	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = z → ((y ∈ A ∧ 0R <R y) ↔ (z ∈ A ∧ 0R <R z)))
88	84, 87, 5	elab2 1419	. . . . . . . . . . . . . . . . . 18 ⊢ (z ∈ B ↔ (z ∈ A ∧ 0R <R z))
89	88	pm3.26bd 259	. . . . . . . . . . . . . . . . 17 ⊢ (z ∈ B → z ∈ A)
90	89	anim1i 269	. . . . . . . . . . . . . . . 16 ⊢ ((z ∈ B ∧ y <R z) → (z ∈ A ∧ y <R z))
91	90	anim2i 270	. . . . . . . . . . . . . . 15 ⊢ ((z ∈ R ∧ (z ∈ B ∧ y <R z)) → (z ∈ R ∧ (z ∈ A ∧ y <R z)))
92	91	19.22i 723	. . . . . . . . . . . . . 14 ⊢ (∃z(z ∈ R ∧ (z ∈ B ∧ y <R z)) → ∃z(z ∈ R ∧ (z ∈ A ∧ y <R z)))
93	92	syl3 18	. . . . . . . . . . . . 13 ⊢ ((y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))) → (y <R x → ∃z(z ∈ R ∧ (z ∈ A ∧ y <R z))))
94	93	syl3 18	. . . . . . . . . . . 12 ⊢ ((y ∈ R → (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z)))) → (y ∈ R → (y <R x → ∃z(z ∈ R ∧ (z ∈ A ∧ y <R z)))))
95	94	a4s 682	. . . . . . . . . . 11 ⊢ (∀y(y ∈ R → (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z)))) → (y ∈ R → (y <R x → ∃z(z ∈ R ∧ (z ∈ A ∧ y <R z)))))
96	95	a1i 7	. . . . . . . . . 10 ⊢ ((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) → (∀y(y ∈ R → (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z)))) → (y ∈ R → (y <R x → ∃z(z ∈ R ∧ (z ∈ A ∧ y <R z))))))
97	83, 96	anim12d 431	. . . . . . . . 9 ⊢ ((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) → ((∀y(y ∈ R → (y ∈ B → ¬ x <R y)) ∧ ∀y(y ∈ R → (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))))) → ((y ∈ R → (y ∈ A → ¬ x <R y)) ∧ (y ∈ R → (y <R x → ∃z(z ∈ R ∧ (z ∈ A ∧ y <R z)))))))
98		jcab 454	. . . . . . . . . . 11 ⊢ ((y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))))) ↔ ((y ∈ R → (y ∈ B → ¬ x <R y)) ∧ (y ∈ R → (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))))))
99	98	bial 695	. . . . . . . . . 10 ⊢ (∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))))) ↔ ∀y((y ∈ R → (y ∈ B → ¬ x <R y)) ∧ (y ∈ R → (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))))))
100		19.26 749	. . . . . . . . . 10 ⊢ (∀y((y ∈ R → (y ∈ B → ¬ x <R y)) ∧ (y ∈ R → (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))))) ↔ (∀y(y ∈ R → (y ∈ B → ¬ x <R y)) ∧ ∀y(y ∈ R → (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))))))
101	99, 100	bitr 151	. . . . . . . . 9 ⊢ (∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))))) ↔ (∀y(y ∈ R → (y ∈ B → ¬ x <R y)) ∧ ∀y(y ∈ R → (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))))))
102		jcab 454	. . . . . . . . 9 ⊢ ((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))))))
103	97, 101, 102	3imtr4g 426	. . . . . . . 8 ⊢ ((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) → (∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))))) → (y ∈ R → ((y ∈ A → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ A ∧ y <R z)))))))
104	103	imp 277	. . . . . . 7 ⊢ (((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) ∧ ∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z)))))) → (y ∈ R → ((y ∈ A → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ A ∧ y <R z))))))
105	27, 104	19.21ai 740	. . . . . 6 ⊢ (((∃y(y ∈ A ∧ 0R <R y) ∧ x ∈ R) ∧ ∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z)))))) → ∀y(y ∈ R → ((y ∈ A → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ A ∧ y <R z))))))
106	105	exp31 293	. . . . 5 ⊢ (∃y(y ∈ A ∧ 0R <R y) → (x ∈ R → (∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z))))) → ∀y(y ∈ R → ((y ∈ A → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ A ∧ y <R z))))))))
107	106	imdistand 342	. . . 4 ⊢ (∃y(y ∈ A ∧ 0R <R y) → ((x ∈ R ∧ ∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ y <R z)))))) → (x ∈ R ∧ ∀y(y ∈ R → ((y ∈ A → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ A ∧ y <R z))))))))
108	107	19.22dv 947	. . 3 ⊢ (∃y(y ∈ A ∧ 0R <R y) → (∃x(x ∈ R ∧ ∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ 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))))))))
109	108	adantr 306	. 2 ⊢ ((∃y(y ∈ A ∧ 0R <R y) ∧ ∃x(x ∈ R ∧ ∀y(y ∈ R → (y ∈ A → y <R x)))) → (∃x(x ∈ R ∧ ∀y(y ∈ R → ((y ∈ B → ¬ x <R y) ∧ (y <R x → ∃z(z ∈ R ∧ (z ∈ B ∧ 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))))))))
110	22, 109	mpd 46	1 ⊢ ((∃y(y ∈ A ∧ 0R <R y) ∧ ∃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 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797  {cab 1090   = wceq 1091   ∈ wcel 1092  ∅c0 1707   class class class wbr 2054   Or wor 2059  Rcnr 3787  0_Rc0r 3788   <_R cltr 3793

This theorem is referenced by:  supsrlem6 4024

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fv 2438  df-rdg 2970  df-opr 3003  df-oprab 3004  df-1o 3104  df-oadd 3106  df-omul 3107  df-er 3200  df-ec 3202  df-qs 3205  df-ni 3794  df-pli 3795  df-mi 3796  df-lti 3797  df-plpq 3829  df-mpq 3830  df-enq 3831  df-nq 3832  df-plq 3833  df-mq 3834  df-rq 3835  df-ltq 3836  df-1q 3837  df-np 3880  df-1p 3881  df-plp 3882  df-ltp 3884  df-enr 3960  df-nr 3961  df-ltr 3964  df-0r 3965

metamath.org