Theorem dedekind 10079

Description: The Dedekind cut theorem. This theorem, which may be used to replace ax-pre-sup 9893 with appropriate adjustments, states that, if 𝐴 completely preceeds 𝐵, then there is some number separating the two of them. (Contributed by Scott Fenton, 13-Jun-2013.)

Assertion

Ref	Expression
dedekind	⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))

Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧

Proof of Theorem dedekind

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1830	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅)
2		nfv 1830	. . . . . . . 8 ⊢ Ⅎ𝑥(𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ)
3		nfra1 2925	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦
4	1, 2, 3	nf3an 1819	. . . . . . 7 ⊢ Ⅎ𝑥((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦)
5		nfv 1830	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑧 ∈ ℝ
6		nfra1 2925	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥
7		nfra1 2925	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)
8	6, 7	nfan 1816	. . . . . . . 8 ⊢ Ⅎ𝑥(∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))
9	5, 8	nfan 1816	. . . . . . 7 ⊢ Ⅎ𝑥(𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))
10	4, 9	nfan 1816	. . . . . 6 ⊢ Ⅎ𝑥(((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))))
11		nfv 1830	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅)
12		nfv 1830	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ)
13		nfra2 2930	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦
14	11, 12, 13	nf3an 1819	. . . . . . . 8 ⊢ Ⅎ𝑦((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦)
15		nfv 1830	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))
16	14, 15	nfan 1816	. . . . . . 7 ⊢ Ⅎ𝑦(((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))))
17		nfv 1830	. . . . . . 7 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
18		simprrl 800	. . . . . . . . . . . 12 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))) → ∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥)
19	18	r19.21bi 2916	. . . . . . . . . . 11 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑧 < 𝑥)
20		simpl2l 1107	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))) → 𝐴 ⊆ ℝ)
21	20	sselda 3568	. . . . . . . . . . . 12 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ)
22		simplrl 796	. . . . . . . . . . . 12 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))) ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ ℝ)
23	21, 22	lenltd 10062	. . . . . . . . . . 11 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≤ 𝑧 ↔ ¬ 𝑧 < 𝑥))
24	19, 23	mpbird 246	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ 𝑧)
25	24	ex 449	. . . . . . . . 9 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))) → (𝑥 ∈ 𝐴 → 𝑥 ≤ 𝑧))
26		simpl3 1059	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ ((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦)
27		simp2 1055	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ))
28		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
29		rsp 2913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝐵 𝑥 < 𝑦 → (𝑦 ∈ 𝐵 → 𝑥 < 𝑦))
30	29	com12 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ 𝐵 → (∀𝑦 ∈ 𝐵 𝑥 < 𝑦 → 𝑥 < 𝑦))
31	30	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (∀𝑦 ∈ 𝐵 𝑥 < 𝑦 → 𝑥 < 𝑦))
32		ssel2 3563	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ)
33	32	adantlr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ)
34	33	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ ℝ)
35		simplr 788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ ℝ)
36	35	sselda 3568	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ)
37		ltnsym 10014	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 < 𝑦 → ¬ 𝑦 < 𝑥))
38	34, 36, 37	syl2anc 691	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑥 < 𝑦 → ¬ 𝑦 < 𝑥))
39	31, 38	syld 46	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (∀𝑦 ∈ 𝐵 𝑥 < 𝑦 → ¬ 𝑦 < 𝑥))
40	39	an32s 842	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝑥 < 𝑦 → ¬ 𝑦 < 𝑥))
41	40	ralimdva 2945	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ 𝑦 ∈ 𝐵) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦 → ∀𝑥 ∈ 𝐴 ¬ 𝑦 < 𝑥))
42	27, 28, 41	syl2an 493	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ ((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦 → ∀𝑥 ∈ 𝐴 ¬ 𝑦 < 𝑥))
43	26, 42	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ ((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵)) → ∀𝑥 ∈ 𝐴 ¬ 𝑦 < 𝑥)
44		breq2 4587	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑦 < 𝑥 ↔ 𝑦 < 𝑤))
45	44	notbid 307	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (¬ 𝑦 < 𝑥 ↔ ¬ 𝑦 < 𝑤))
46	45	cbvralv 3147	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑦 < 𝑥 ↔ ∀𝑤 ∈ 𝐴 ¬ 𝑦 < 𝑤)
47	43, 46	sylib 207	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ ((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵)) → ∀𝑤 ∈ 𝐴 ¬ 𝑦 < 𝑤)
48		ralnex 2975	. . . . . . . . . . . . 13 ⊢ (∀𝑤 ∈ 𝐴 ¬ 𝑦 < 𝑤 ↔ ¬ ∃𝑤 ∈ 𝐴 𝑦 < 𝑤)
49	47, 48	sylib 207	. . . . . . . . . . . 12 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ ((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵)) → ¬ ∃𝑤 ∈ 𝐴 𝑦 < 𝑤)
50		simp2r 1081	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → 𝐵 ⊆ ℝ)
51		ssel2 3563	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ⊆ ℝ ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ)
52	50, 28, 51	syl2an 493	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ ((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ ℝ)
53		simplrr 797	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵) → ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))
54	53	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ ((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵)) → ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))
55		breq1 4586	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑥 < 𝑧 ↔ 𝑦 < 𝑧))
56		breq1 4586	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥 < 𝑤 ↔ 𝑦 < 𝑤))
57	56	rexbidv 3034	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (∃𝑤 ∈ 𝐴 𝑥 < 𝑤 ↔ ∃𝑤 ∈ 𝐴 𝑦 < 𝑤))
58	55, 57	imbi12d 333	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤) ↔ (𝑦 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑦 < 𝑤)))
59	58	rspcv 3278	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → (∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤) → (𝑦 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑦 < 𝑤)))
60	52, 54, 59	sylc 63	. . . . . . . . . . . 12 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ ((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵)) → (𝑦 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑦 < 𝑤))
61	49, 60	mtod 188	. . . . . . . . . . 11 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ ((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵)) → ¬ 𝑦 < 𝑧)
62		simprll 798	. . . . . . . . . . . 12 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ ((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵)) → 𝑧 ∈ ℝ)
63	62, 52	lenltd 10062	. . . . . . . . . . 11 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ ((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵)) → (𝑧 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑧))
64	61, 63	mpbird 246	. . . . . . . . . 10 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ ((𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤))) ∧ 𝑦 ∈ 𝐵)) → 𝑧 ≤ 𝑦)
65	64	expr 641	. . . . . . . . 9 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))) → (𝑦 ∈ 𝐵 → 𝑧 ≤ 𝑦))
66	25, 65	anim12d 584	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)))
67	66	expd 451	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))))
68	16, 17, 67	ralrimd 2942	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))) → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)))
69	10, 68	ralrimi 2940	. . . . 5 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) ∧ (𝑧 ∈ ℝ ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))
70		simp2l 1080	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → 𝐴 ⊆ ℝ)
71		simp1l 1078	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → 𝐴 ≠ ∅)
72		simp1r 1079	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → 𝐵 ≠ ∅)
73		n0 3890	. . . . . . . . 9 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝐵)
74	72, 73	sylib 207	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧 𝑧 ∈ 𝐵)
75	50	sseld 3567	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → (𝑧 ∈ 𝐵 → 𝑧 ∈ ℝ))
76		ralcom 3079	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝑥 < 𝑦)
77		breq2 4587	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (𝑥 < 𝑦 ↔ 𝑥 < 𝑧))
78	77	ralbidv 2969	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (∀𝑥 ∈ 𝐴 𝑥 < 𝑦 ↔ ∀𝑥 ∈ 𝐴 𝑥 < 𝑧))
79	78	rspccv 3279	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝑥 < 𝑦 → (𝑧 ∈ 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 < 𝑧))
80	76, 79	sylbi 206	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦 → (𝑧 ∈ 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 < 𝑧))
81	80	3ad2ant3 1077	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → (𝑧 ∈ 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 < 𝑧))
82	75, 81	jcad 554	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → (𝑧 ∈ 𝐵 → (𝑧 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 < 𝑧)))
83	82	eximdv 1833	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → (∃𝑧 𝑧 ∈ 𝐵 → ∃𝑧(𝑧 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 < 𝑧)))
84	74, 83	mpd 15	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧(𝑧 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 < 𝑧))
85		df-rex 2902	. . . . . . 7 ⊢ (∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 < 𝑧 ↔ ∃𝑧(𝑧 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 < 𝑧))
86	84, 85	sylibr 223	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 < 𝑧)
87		axsup 9992	. . . . . 6 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 < 𝑧) → ∃𝑧 ∈ ℝ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))
88	70, 71, 86, 87	syl3anc 1318	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧 ∈ ℝ (∀𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝑧 → ∃𝑤 ∈ 𝐴 𝑥 < 𝑤)))
89	69, 88	reximddv 3001	. . . 4 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))
90	89	3expib 1260	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)))
91		1re 9918	. . . . 5 ⊢ 1 ∈ ℝ
92		rzal 4025	. . . . 5 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 1 ∧ 1 ≤ 𝑦))
93		breq2 4587	. . . . . . . 8 ⊢ (𝑧 = 1 → (𝑥 ≤ 𝑧 ↔ 𝑥 ≤ 1))
94		breq1 4586	. . . . . . . 8 ⊢ (𝑧 = 1 → (𝑧 ≤ 𝑦 ↔ 1 ≤ 𝑦))
95	93, 94	anbi12d 743	. . . . . . 7 ⊢ (𝑧 = 1 → ((𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) ↔ (𝑥 ≤ 1 ∧ 1 ≤ 𝑦)))
96	95	2ralbidv 2972	. . . . . 6 ⊢ (𝑧 = 1 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 1 ∧ 1 ≤ 𝑦)))
97	96	rspcev 3282	. . . . 5 ⊢ ((1 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 1 ∧ 1 ≤ 𝑦)) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))
98	91, 92, 97	sylancr 694	. . . 4 ⊢ (𝐴 = ∅ → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))
99	98	a1d 25	. . 3 ⊢ (𝐴 = ∅ → (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)))
100		rzal 4025	. . . . . 6 ⊢ (𝐵 = ∅ → ∀𝑦 ∈ 𝐵 (𝑥 ≤ 1 ∧ 1 ≤ 𝑦))
101	100	ralrimivw 2950	. . . . 5 ⊢ (𝐵 = ∅ → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 1 ∧ 1 ≤ 𝑦))
102	91, 101, 97	sylancr 694	. . . 4 ⊢ (𝐵 = ∅ → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))
103	102	a1d 25	. . 3 ⊢ (𝐵 = ∅ → (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)))
104	90, 99, 103	pm2.61iine 2872	. 2 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))
105	104	3impa 1251	1 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583  ℝcr 9814  1c1 9816   < clt 9953   ≤ cle 9954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-sup 9893

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959

This theorem is referenced by:  dedekindle  10080