supsrlem

Description: Lemma for supremum theorem. (Contributed by NM, 21-May-1996) (Revised by Mario Carneiro, 15-Jun-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	supsrlem.1	$⊢ B = \{w \| C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} \in A\}$
	supsrlem.2	$⊢ C \in 𝑹$
Assertion	supsrlem	$⊢ (C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \to \exists x \in 𝑹 (\forall y \in A \neg x <_{𝑹} y \land \forall y \in 𝑹 (y <_{𝑹} x \to \exists z \in A y <_{𝑹} z))$

Proof

Step	Hyp	Ref	Expression
1		supsrlem.1	$⊢ B = \{w \| C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} \in A\}$
2		supsrlem.2	$⊢ C \in 𝑹$
3		0idsr	$⊢ C \in 𝑹 \to C +_{𝑹} 0_{𝑹} = C$
4	2 3	mp1i	$⊢ (C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \to C +_{𝑹} 0_{𝑹} = C$
5		simpl	$⊢ (C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \to C \in A$
6	4 5	eqeltrd	$⊢ (C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \to C +_{𝑹} 0_{𝑹} \in A$
7		1pr	$⊢ 1_{𝑷} \in 𝑷$
8	7	elexi	$⊢ 1_{𝑷} \in V$
9		opeq1	$⊢ w = 1_{𝑷} \to ⟨w, 1_{𝑷}⟩ = ⟨1_{𝑷}, 1_{𝑷}⟩$
10	9	eceq1d	$⊢ w = 1_{𝑷} \to [⟨w, 1_{𝑷}⟩] ~_{𝑹} = [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
11		df-0r	$⊢ 0_{𝑹} = [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
12	10 11	eqtr4di	$⊢ w = 1_{𝑷} \to [⟨w, 1_{𝑷}⟩] ~_{𝑹} = 0_{𝑹}$
13	12	oveq2d	$⊢ w = 1_{𝑷} \to C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = C +_{𝑹} 0_{𝑹}$
14	13	eleq1d	$⊢ w = 1_{𝑷} \to (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} \in A \leftrightarrow C +_{𝑹} 0_{𝑹} \in A)$
15	8 14 1	elab2	$⊢ 1_{𝑷} \in B \leftrightarrow C +_{𝑹} 0_{𝑹} \in A$
16	6 15	sylibr	$⊢ (C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \to 1_{𝑷} \in B$
17	16	ne0d	$⊢ (C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \to B \neq \emptyset$
18		breq1	$⊢ y = C \to (y <_{𝑹} x \leftrightarrow C <_{𝑹} x)$
19	18	rspccv	$⊢ \forall y \in A y <_{𝑹} x \to (C \in A \to C <_{𝑹} x)$
20		0lt1sr	$⊢ 0_{𝑹} <_{𝑹} 1_{𝑹}$
21		m1r	$⊢ {-1}_{𝑹} \in 𝑹$
22		ltasr	$⊢ {-1}_{𝑹} \in 𝑹 \to (0_{𝑹} <_{𝑹} 1_{𝑹} \leftrightarrow ({-1}_{𝑹} +_{𝑹} 0_{𝑹}) <_{𝑹} ({-1}_{𝑹} +_{𝑹} 1_{𝑹}))$
23	21 22	ax-mp	$⊢ 0_{𝑹} <_{𝑹} 1_{𝑹} \leftrightarrow ({-1}_{𝑹} +_{𝑹} 0_{𝑹}) <_{𝑹} ({-1}_{𝑹} +_{𝑹} 1_{𝑹})$
24	20 23	mpbi	$⊢ ({-1}_{𝑹} +_{𝑹} 0_{𝑹}) <_{𝑹} ({-1}_{𝑹} +_{𝑹} 1_{𝑹})$
25		0idsr	$⊢ {-1}_{𝑹} \in 𝑹 \to {-1}_{𝑹} +_{𝑹} 0_{𝑹} = {-1}_{𝑹}$
26	21 25	ax-mp	$⊢ {-1}_{𝑹} +_{𝑹} 0_{𝑹} = {-1}_{𝑹}$
27		m1p1sr	$⊢ {-1}_{𝑹} +_{𝑹} 1_{𝑹} = 0_{𝑹}$
28	24 26 27	3brtr3i	$⊢ {-1}_{𝑹} <_{𝑹} 0_{𝑹}$
29		ltasr	$⊢ C \in 𝑹 \to ({-1}_{𝑹} <_{𝑹} 0_{𝑹} \leftrightarrow (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} (C +_{𝑹} 0_{𝑹}))$
30	2 29	ax-mp	$⊢ {-1}_{𝑹} <_{𝑹} 0_{𝑹} \leftrightarrow (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} (C +_{𝑹} 0_{𝑹})$
31	28 30	mpbi	$⊢ (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} (C +_{𝑹} 0_{𝑹})$
32	2 3	ax-mp	$⊢ C +_{𝑹} 0_{𝑹} = C$
33	31 32	breqtri	$⊢ (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} C$
34		ltsosr	$⊢ <_{𝑹} Or 𝑹$
35		ltrelsr	$⊢ <_{𝑹} \subseteq 𝑹 \times 𝑹$
36	34 35	sotri	$⊢ ((C +_{𝑹} {-1}_{𝑹}) <_{𝑹} C \land C <_{𝑹} x) \to (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} x$
37	33 36	mpan	$⊢ C <_{𝑹} x \to (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} x$
38	2	map2psrpr	$⊢ (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} x \leftrightarrow \exists v \in 𝑷 C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} = x$
39	37 38	sylib	$⊢ C <_{𝑹} x \to \exists v \in 𝑷 C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} = x$
40	19 39	syl6	$⊢ \forall y \in A y <_{𝑹} x \to (C \in A \to \exists v \in 𝑷 C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} = x)$
41		breq2	$⊢ C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} = x \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \leftrightarrow y <_{𝑹} x)$
42	41	ralbidv	$⊢ C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} = x \to (\forall y \in A y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \leftrightarrow \forall y \in A y <_{𝑹} x)$
43	1	abeq2i	$⊢ w \in B \leftrightarrow C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} \in A$
44		breq1	$⊢ y = C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \leftrightarrow (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}))$
45	44	rspccv	$⊢ \forall y \in A y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} \in A \to (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}))$
46	2	ltpsrpr	$⊢ (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \leftrightarrow w <_{𝑷} v$
47	45 46	syl6ib	$⊢ \forall y \in A y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} \in A \to w <_{𝑷} v)$
48	43 47	syl5bi	$⊢ \forall y \in A y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to (w \in B \to w <_{𝑷} v)$
49	48	ralrimiv	$⊢ \forall y \in A y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \forall w \in B w <_{𝑷} v$
50	42 49	syl6bir	$⊢ C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} = x \to (\forall y \in A y <_{𝑹} x \to \forall w \in B w <_{𝑷} v)$
51	50	com12	$⊢ \forall y \in A y <_{𝑹} x \to (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} = x \to \forall w \in B w <_{𝑷} v)$
52	51	reximdv	$⊢ \forall y \in A y <_{𝑹} x \to (\exists v \in 𝑷 C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} = x \to \exists v \in 𝑷 \forall w \in B w <_{𝑷} v)$
53	40 52	syld	$⊢ \forall y \in A y <_{𝑹} x \to (C \in A \to \exists v \in 𝑷 \forall w \in B w <_{𝑷} v)$
54	53	rexlimivw	$⊢ \exists x \in 𝑹 \forall y \in A y <_{𝑹} x \to (C \in A \to \exists v \in 𝑷 \forall w \in B w <_{𝑷} v)$
55	54	impcom	$⊢ (C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \to \exists v \in 𝑷 \forall w \in B w <_{𝑷} v$
56		supexpr	$⊢ (B \neq \emptyset \land \exists v \in 𝑷 \forall w \in B w <_{𝑷} v) \to \exists v \in 𝑷 (\forall w \in B \neg v <_{𝑷} w \land \forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u))$
57	17 55 56	syl2anc	$⊢ (C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \to \exists v \in 𝑷 (\forall w \in B \neg v <_{𝑷} w \land \forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u))$
58	2	mappsrpr	$⊢ (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \leftrightarrow v \in 𝑷$
59	35	brel	$⊢ (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to (C +_{𝑹} {-1}_{𝑹} \in 𝑹 \land C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \in 𝑹)$
60	58 59	sylbir	$⊢ v \in 𝑷 \to (C +_{𝑹} {-1}_{𝑹} \in 𝑹 \land C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \in 𝑹)$
61	60	simprd	$⊢ v \in 𝑷 \to C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \in 𝑹$
62	61	adantl	$⊢ ((C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \land v \in 𝑷) \to C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \in 𝑹$
63	34 35	sotri	$⊢ ((C +_{𝑹} {-1}_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \land (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y) \to (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} y$
64	58 63	sylanbr	$⊢ (v \in 𝑷 \land (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y) \to (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} y$
65	2	map2psrpr	$⊢ (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} y \leftrightarrow \exists w \in 𝑷 C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y$
66	64 65	sylib	$⊢ (v \in 𝑷 \land (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y) \to \exists w \in 𝑷 C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y$
67		rexex	$⊢ \exists w \in 𝑷 C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to \exists w C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y$
68		df-ral	$⊢ \forall w \in B \neg v <_{𝑷} w \leftrightarrow \forall w (w \in B \to \neg v <_{𝑷} w)$
69		19.29	$⊢ (\forall w (w \in B \to \neg v <_{𝑷} w) \land \exists w C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y) \to \exists w ((w \in B \to \neg v <_{𝑷} w) \land C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y)$
70		eleq1	$⊢ C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} \in A \leftrightarrow y \in A)$
71	43 70	syl5bb	$⊢ C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to (w \in B \leftrightarrow y \in A)$
72	2	ltpsrpr	$⊢ (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) \leftrightarrow v <_{𝑷} w$
73		breq2	$⊢ C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to ((C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) \leftrightarrow (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
74	72 73	bitr3id	$⊢ C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to (v <_{𝑷} w \leftrightarrow (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
75	74	notbid	$⊢ C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to (\neg v <_{𝑷} w \leftrightarrow \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
76	71 75	imbi12d	$⊢ C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to ((w \in B \to \neg v <_{𝑷} w) \leftrightarrow (y \in A \to \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y))$
77	76	biimpac	$⊢ ((w \in B \to \neg v <_{𝑷} w) \land C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y) \to (y \in A \to \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
78	77	exlimiv	$⊢ \exists w ((w \in B \to \neg v <_{𝑷} w) \land C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y) \to (y \in A \to \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
79	69 78	syl	$⊢ (\forall w (w \in B \to \neg v <_{𝑷} w) \land \exists w C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y) \to (y \in A \to \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
80	68 79	sylanb	$⊢ (\forall w \in B \neg v <_{𝑷} w \land \exists w C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y) \to (y \in A \to \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
81	80	expcom	$⊢ \exists w C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to (\forall w \in B \neg v <_{𝑷} w \to (y \in A \to \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y))$
82	66 67 81	3syl	$⊢ (v \in 𝑷 \land (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y) \to (\forall w \in B \neg v <_{𝑷} w \to (y \in A \to \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y))$
83	82	impd	$⊢ (v \in 𝑷 \land (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y) \to ((\forall w \in B \neg v <_{𝑷} w \land y \in A) \to \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
84	83	impancom	$⊢ (v \in 𝑷 \land (\forall w \in B \neg v <_{𝑷} w \land y \in A)) \to ((C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y \to \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
85	84	pm2.01d	$⊢ (v \in 𝑷 \land (\forall w \in B \neg v <_{𝑷} w \land y \in A)) \to \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y$
86	85	expr	$⊢ (v \in 𝑷 \land \forall w \in B \neg v <_{𝑷} w) \to (y \in A \to \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
87	86	ralrimiv	$⊢ (v \in 𝑷 \land \forall w \in B \neg v <_{𝑷} w) \to \forall y \in A \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y$
88	87	ex	$⊢ v \in 𝑷 \to (\forall w \in B \neg v <_{𝑷} w \to \forall y \in A \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
89	88	adantl	$⊢ ((C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \land v \in 𝑷) \to (\forall w \in B \neg v <_{𝑷} w \to \forall y \in A \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
90		r19.29	$⊢ (\forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u) \land \exists w \in 𝑷 C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y) \to \exists w \in 𝑷 ((w <_{𝑷} v \to \exists u \in B w <_{𝑷} u) \land C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y)$
91		breq1	$⊢ C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to ((C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \leftrightarrow y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}))$
92	46 91	bitr3id	$⊢ C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to (w <_{𝑷} v \leftrightarrow y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}))$
93	92	biimprd	$⊢ C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to w <_{𝑷} v)$
94		vex	$⊢ u \in V$
95		opeq1	$⊢ w = u \to ⟨w, 1_{𝑷}⟩ = ⟨u, 1_{𝑷}⟩$
96	95	eceq1d	$⊢ w = u \to [⟨w, 1_{𝑷}⟩] ~_{𝑹} = [⟨u, 1_{𝑷}⟩] ~_{𝑹}$
97	96	oveq2d	$⊢ w = u \to C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = C +_{𝑹} [⟨u, 1_{𝑷}⟩] ~_{𝑹}$
98	97	eleq1d	$⊢ w = u \to (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} \in A \leftrightarrow C +_{𝑹} [⟨u, 1_{𝑷}⟩] ~_{𝑹} \in A)$
99	94 98 1	elab2	$⊢ u \in B \leftrightarrow C +_{𝑹} [⟨u, 1_{𝑷}⟩] ~_{𝑹} \in A$
100		breq2	$⊢ z = C +_{𝑹} [⟨u, 1_{𝑷}⟩] ~_{𝑹} \to ((C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} z \leftrightarrow (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨u, 1_{𝑷}⟩] ~_{𝑹}))$
101	2	ltpsrpr	$⊢ (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} (C +_{𝑹} [⟨u, 1_{𝑷}⟩] ~_{𝑹}) \leftrightarrow w <_{𝑷} u$
102	100 101	bitrdi	$⊢ z = C +_{𝑹} [⟨u, 1_{𝑷}⟩] ~_{𝑹} \to ((C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} z \leftrightarrow w <_{𝑷} u)$
103	102	rspcev	$⊢ (C +_{𝑹} [⟨u, 1_{𝑷}⟩] ~_{𝑹} \in A \land w <_{𝑷} u) \to \exists z \in A (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} z$
104	99 103	sylanb	$⊢ (u \in B \land w <_{𝑷} u) \to \exists z \in A (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} z$
105	104	rexlimiva	$⊢ \exists u \in B w <_{𝑷} u \to \exists z \in A (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} z$
106		breq1	$⊢ C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to ((C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} z \leftrightarrow y <_{𝑹} z)$
107	106	rexbidv	$⊢ C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to (\exists z \in A (C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} z \leftrightarrow \exists z \in A y <_{𝑹} z)$
108	105 107	syl5ib	$⊢ C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to (\exists u \in B w <_{𝑷} u \to \exists z \in A y <_{𝑹} z)$
109	93 108	imim12d	$⊢ C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y \to ((w <_{𝑷} v \to \exists u \in B w <_{𝑷} u) \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z))$
110	109	impcom	$⊢ ((w <_{𝑷} v \to \exists u \in B w <_{𝑷} u) \land C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y) \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z)$
111	110	rexlimivw	$⊢ \exists w \in 𝑷 ((w <_{𝑷} v \to \exists u \in B w <_{𝑷} u) \land C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y) \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z)$
112	90 111	syl	$⊢ (\forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u) \land \exists w \in 𝑷 C +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} = y) \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z)$
113	65 112	sylan2b	$⊢ (\forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u) \land (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} y) \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z)$
114	113	ex	$⊢ \forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u) \to ((C +_{𝑹} {-1}_{𝑹}) <_{𝑹} y \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z))$
115	114	adantl	$⊢ ((C \in A \land v \in 𝑷) \land \forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u)) \to ((C +_{𝑹} {-1}_{𝑹}) <_{𝑹} y \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z))$
116	115	a1dd	$⊢ ((C \in A \land v \in 𝑷) \land \forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u)) \to ((C +_{𝑹} {-1}_{𝑹}) <_{𝑹} y \to (y \in 𝑹 \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z)))$
117	34 35	sotri2	$⊢ (y \in 𝑹 \land \neg (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} y \land (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} C) \to y <_{𝑹} C$
118	33 117	mp3an3	$⊢ (y \in 𝑹 \land \neg (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} y) \to y <_{𝑹} C$
119		breq2	$⊢ z = C \to (y <_{𝑹} z \leftrightarrow y <_{𝑹} C)$
120	119	rspcev	$⊢ (C \in A \land y <_{𝑹} C) \to \exists z \in A y <_{𝑹} z$
121	120	ex	$⊢ C \in A \to (y <_{𝑹} C \to \exists z \in A y <_{𝑹} z)$
122	121	a1dd	$⊢ C \in A \to (y <_{𝑹} C \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z))$
123	118 122	syl5	$⊢ C \in A \to ((y \in 𝑹 \land \neg (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} y) \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z))$
124	123	expcomd	$⊢ C \in A \to (\neg (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} y \to (y \in 𝑹 \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z)))$
125	124	ad2antrr	$⊢ ((C \in A \land v \in 𝑷) \land \forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u)) \to (\neg (C +_{𝑹} {-1}_{𝑹}) <_{𝑹} y \to (y \in 𝑹 \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z)))$
126	116 125	pm2.61d	$⊢ ((C \in A \land v \in 𝑷) \land \forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u)) \to (y \in 𝑹 \to (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z))$
127	126	ralrimiv	$⊢ ((C \in A \land v \in 𝑷) \land \forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u)) \to \forall y \in 𝑹 (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z)$
128	127	ex	$⊢ (C \in A \land v \in 𝑷) \to (\forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u) \to \forall y \in 𝑹 (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z))$
129	128	adantlr	$⊢ ((C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \land v \in 𝑷) \to (\forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u) \to \forall y \in 𝑹 (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z))$
130	89 129	anim12d	$⊢ ((C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \land v \in 𝑷) \to ((\forall w \in B \neg v <_{𝑷} w \land \forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u)) \to (\forall y \in A \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y \land \forall y \in 𝑹 (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z)))$
131		breq1	$⊢ x = C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \to (x <_{𝑹} y \leftrightarrow (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
132	131	notbid	$⊢ x = C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \to (\neg x <_{𝑹} y \leftrightarrow \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
133	132	ralbidv	$⊢ x = C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \to (\forall y \in A \neg x <_{𝑹} y \leftrightarrow \forall y \in A \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y)$
134		breq2	$⊢ x = C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \to (y <_{𝑹} x \leftrightarrow y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}))$
135	134	imbi1d	$⊢ x = C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \to ((y <_{𝑹} x \to \exists z \in A y <_{𝑹} z) \leftrightarrow (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z))$
136	135	ralbidv	$⊢ x = C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \to (\forall y \in 𝑹 (y <_{𝑹} x \to \exists z \in A y <_{𝑹} z) \leftrightarrow \forall y \in 𝑹 (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z))$
137	133 136	anbi12d	$⊢ x = C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \to ((\forall y \in A \neg x <_{𝑹} y \land \forall y \in 𝑹 (y <_{𝑹} x \to \exists z \in A y <_{𝑹} z)) \leftrightarrow (\forall y \in A \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y \land \forall y \in 𝑹 (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z)))$
138	137	rspcev	$⊢ (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \in 𝑹 \land (\forall y \in A \neg (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) <_{𝑹} y \land \forall y \in 𝑹 (y <_{𝑹} (C +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹}) \to \exists z \in A y <_{𝑹} z))) \to \exists x \in 𝑹 (\forall y \in A \neg x <_{𝑹} y \land \forall y \in 𝑹 (y <_{𝑹} x \to \exists z \in A y <_{𝑹} z))$
139	62 130 138	syl6an	$⊢ ((C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \land v \in 𝑷) \to ((\forall w \in B \neg v <_{𝑷} w \land \forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u)) \to \exists x \in 𝑹 (\forall y \in A \neg x <_{𝑹} y \land \forall y \in 𝑹 (y <_{𝑹} x \to \exists z \in A y <_{𝑹} z)))$
140	139	rexlimdva	$⊢ (C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \to (\exists v \in 𝑷 (\forall w \in B \neg v <_{𝑷} w \land \forall w \in 𝑷 (w <_{𝑷} v \to \exists u \in B w <_{𝑷} u)) \to \exists x \in 𝑹 (\forall y \in A \neg x <_{𝑹} y \land \forall y \in 𝑹 (y <_{𝑹} x \to \exists z \in A y <_{𝑹} z)))$
141	57 140	mpd	$⊢ (C \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \to \exists x \in 𝑹 (\forall y \in A \neg x <_{𝑹} y \land \forall y \in 𝑹 (y <_{𝑹} x \to \exists z \in A y <_{𝑹} z))$

Metamath Proof Explorer

Theorem supsrlem

Proof