Metamath Proof Explorer

Theorem 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+𝑹w1𝑷~𝑹∈A
supsrlem.2 ⊢C∈𝑹
Assertion supsrlem ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z

Proof

Step Hyp Ref Expression
1 supsrlem.1 ⊢B=w|C+𝑹w1𝑷~𝑹∈A
2 supsrlem.2 ⊢C∈𝑹
3 0idsr ⊢C∈𝑹→C+𝑹0𝑹=C
4 2 3 mp1i ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x→C+𝑹0𝑹=C
5 simpl ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x→C∈A
6 4 5 eqeltrd ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x→C+𝑹0𝑹∈A
7 1pr ⊢1𝑷∈𝑷
8 7 elexi ⊢1𝑷∈V
9 opeq1 ⊢w=1𝑷→w1𝑷=1𝑷1𝑷
10 9 eceq1d ⊢w=1𝑷→w1𝑷~𝑹=1𝑷1𝑷~𝑹
11 df-0r ⊢0𝑹=1𝑷1𝑷~𝑹
12 10 11 eqtr4di ⊢w=1𝑷→w1𝑷~𝑹=0𝑹
13 12 oveq2d ⊢w=1𝑷→C+𝑹w1𝑷~𝑹=C+𝑹0𝑹
14 13 eleq1d ⊢w=1𝑷→C+𝑹w1𝑷~𝑹∈A↔C+𝑹0𝑹∈A
15 8 14 1 elab2 ⊢1𝑷∈B↔C+𝑹0𝑹∈A
16 6 15 sylibr ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x→1𝑷∈B
17 16 ne0d ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x→B≠∅
18 breq1 ⊢y=C→y<𝑹x↔C<𝑹x
19 18 rspccv ⊢∀y∈Ay<𝑹x→C∈A→C<𝑹x
20 0lt1sr ⊢0𝑹<𝑹1𝑹
21 m1r ⊢-1𝑹∈𝑹
22 ltasr ⊢-1𝑹∈𝑹→0𝑹<𝑹1𝑹↔-1𝑹+𝑹0𝑹<𝑹-1𝑹+𝑹1𝑹
23 21 22 ax-mp ⊢0𝑹<𝑹1𝑹↔-1𝑹+𝑹0𝑹<𝑹-1𝑹+𝑹1𝑹
24 20 23 mpbi ⊢-1𝑹+𝑹0𝑹<𝑹-1𝑹+𝑹1𝑹
25 0idsr ⊢-1𝑹∈𝑹→-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∈𝑹→-1𝑹<𝑹0𝑹↔C+𝑹-1𝑹<𝑹C+𝑹0𝑹
30 2 29 ax-mp ⊢-1𝑹<𝑹0𝑹↔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 ⊢<𝑹⊆𝑹×𝑹
36 34 35 sotri ⊢C+𝑹-1𝑹<𝑹C∧C<𝑹x→C+𝑹-1𝑹<𝑹x
37 33 36 mpan ⊢C<𝑹x→C+𝑹-1𝑹<𝑹x
38 2 map2psrpr ⊢C+𝑹-1𝑹<𝑹x↔∃v∈𝑷C+𝑹v1𝑷~𝑹=x
39 37 38 sylib ⊢C<𝑹x→∃v∈𝑷C+𝑹v1𝑷~𝑹=x
40 19 39 syl6 ⊢∀y∈Ay<𝑹x→C∈A→∃v∈𝑷C+𝑹v1𝑷~𝑹=x
41 breq2 ⊢C+𝑹v1𝑷~𝑹=x→y<𝑹C+𝑹v1𝑷~𝑹↔y<𝑹x
42 41 ralbidv ⊢C+𝑹v1𝑷~𝑹=x→∀y∈Ay<𝑹C+𝑹v1𝑷~𝑹↔∀y∈Ay<𝑹x
43 1 eqabri ⊢w∈B↔C+𝑹w1𝑷~𝑹∈A
44 breq1 ⊢y=C+𝑹w1𝑷~𝑹→y<𝑹C+𝑹v1𝑷~𝑹↔C+𝑹w1𝑷~𝑹<𝑹C+𝑹v1𝑷~𝑹
45 44 rspccv ⊢∀y∈Ay<𝑹C+𝑹v1𝑷~𝑹→C+𝑹w1𝑷~𝑹∈A→C+𝑹w1𝑷~𝑹<𝑹C+𝑹v1𝑷~𝑹
46 2 ltpsrpr ⊢C+𝑹w1𝑷~𝑹<𝑹C+𝑹v1𝑷~𝑹↔w<𝑷v
47 45 46 imbitrdi ⊢∀y∈Ay<𝑹C+𝑹v1𝑷~𝑹→C+𝑹w1𝑷~𝑹∈A→w<𝑷v
48 43 47 biimtrid ⊢∀y∈Ay<𝑹C+𝑹v1𝑷~𝑹→w∈B→w<𝑷v
49 48 ralrimiv ⊢∀y∈Ay<𝑹C+𝑹v1𝑷~𝑹→∀w∈Bw<𝑷v
50 42 49 syl6bir ⊢C+𝑹v1𝑷~𝑹=x→∀y∈Ay<𝑹x→∀w∈Bw<𝑷v
51 50 com12 ⊢∀y∈Ay<𝑹x→C+𝑹v1𝑷~𝑹=x→∀w∈Bw<𝑷v
52 51 reximdv ⊢∀y∈Ay<𝑹x→∃v∈𝑷C+𝑹v1𝑷~𝑹=x→∃v∈𝑷∀w∈Bw<𝑷v
53 40 52 syld ⊢∀y∈Ay<𝑹x→C∈A→∃v∈𝑷∀w∈Bw<𝑷v
54 53 rexlimivw ⊢∃x∈𝑹∀y∈Ay<𝑹x→C∈A→∃v∈𝑷∀w∈Bw<𝑷v
55 54 impcom ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x→∃v∈𝑷∀w∈Bw<𝑷v
56 supexpr ⊢B≠∅∧∃v∈𝑷∀w∈Bw<𝑷v→∃v∈𝑷∀w∈B¬v<𝑷w∧∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u
57 17 55 56 syl2anc ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x→∃v∈𝑷∀w∈B¬v<𝑷w∧∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u
58 2 mappsrpr ⊢C+𝑹-1𝑹<𝑹C+𝑹v1𝑷~𝑹↔v∈𝑷
59 35 brel ⊢C+𝑹-1𝑹<𝑹C+𝑹v1𝑷~𝑹→C+𝑹-1𝑹∈𝑹∧C+𝑹v1𝑷~𝑹∈𝑹
60 58 59 sylbir ⊢v∈𝑷→C+𝑹-1𝑹∈𝑹∧C+𝑹v1𝑷~𝑹∈𝑹
61 60 simprd ⊢v∈𝑷→C+𝑹v1𝑷~𝑹∈𝑹
62 61 adantl ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x∧v∈𝑷→C+𝑹v1𝑷~𝑹∈𝑹
63 34 35 sotri ⊢C+𝑹-1𝑹<𝑹C+𝑹v1𝑷~𝑹∧C+𝑹v1𝑷~𝑹<𝑹y→C+𝑹-1𝑹<𝑹y
64 58 63 sylanbr ⊢v∈𝑷∧C+𝑹v1𝑷~𝑹<𝑹y→C+𝑹-1𝑹<𝑹y
65 2 map2psrpr ⊢C+𝑹-1𝑹<𝑹y↔∃w∈𝑷C+𝑹w1𝑷~𝑹=y
66 64 65 sylib ⊢v∈𝑷∧C+𝑹v1𝑷~𝑹<𝑹y→∃w∈𝑷C+𝑹w1𝑷~𝑹=y
67 rexex ⊢∃w∈𝑷C+𝑹w1𝑷~𝑹=y→∃wC+𝑹w1𝑷~𝑹=y
68 df-ral ⊢∀w∈B¬v<𝑷w↔∀ww∈B→¬v<𝑷w
69 19.29 ⊢∀ww∈B→¬v<𝑷w∧∃wC+𝑹w1𝑷~𝑹=y→∃ww∈B→¬v<𝑷w∧C+𝑹w1𝑷~𝑹=y
70 eleq1 ⊢C+𝑹w1𝑷~𝑹=y→C+𝑹w1𝑷~𝑹∈A↔y∈A
71 43 70 bitrid ⊢C+𝑹w1𝑷~𝑹=y→w∈B↔y∈A
72 2 ltpsrpr ⊢C+𝑹v1𝑷~𝑹<𝑹C+𝑹w1𝑷~𝑹↔v<𝑷w
73 breq2 ⊢C+𝑹w1𝑷~𝑹=y→C+𝑹v1𝑷~𝑹<𝑹C+𝑹w1𝑷~𝑹↔C+𝑹v1𝑷~𝑹<𝑹y
74 72 73 bitr3id ⊢C+𝑹w1𝑷~𝑹=y→v<𝑷w↔C+𝑹v1𝑷~𝑹<𝑹y
75 74 notbid ⊢C+𝑹w1𝑷~𝑹=y→¬v<𝑷w↔¬C+𝑹v1𝑷~𝑹<𝑹y
76 71 75 imbi12d ⊢C+𝑹w1𝑷~𝑹=y→w∈B→¬v<𝑷w↔y∈A→¬C+𝑹v1𝑷~𝑹<𝑹y
77 76 biimpac ⊢w∈B→¬v<𝑷w∧C+𝑹w1𝑷~𝑹=y→y∈A→¬C+𝑹v1𝑷~𝑹<𝑹y
78 77 exlimiv ⊢∃ww∈B→¬v<𝑷w∧C+𝑹w1𝑷~𝑹=y→y∈A→¬C+𝑹v1𝑷~𝑹<𝑹y
79 69 78 syl ⊢∀ww∈B→¬v<𝑷w∧∃wC+𝑹w1𝑷~𝑹=y→y∈A→¬C+𝑹v1𝑷~𝑹<𝑹y
80 68 79 sylanb ⊢∀w∈B¬v<𝑷w∧∃wC+𝑹w1𝑷~𝑹=y→y∈A→¬C+𝑹v1𝑷~𝑹<𝑹y
81 80 expcom ⊢∃wC+𝑹w1𝑷~𝑹=y→∀w∈B¬v<𝑷w→y∈A→¬C+𝑹v1𝑷~𝑹<𝑹y
82 66 67 81 3syl ⊢v∈𝑷∧C+𝑹v1𝑷~𝑹<𝑹y→∀w∈B¬v<𝑷w→y∈A→¬C+𝑹v1𝑷~𝑹<𝑹y
83 82 impd ⊢v∈𝑷∧C+𝑹v1𝑷~𝑹<𝑹y→∀w∈B¬v<𝑷w∧y∈A→¬C+𝑹v1𝑷~𝑹<𝑹y
84 83 impancom ⊢v∈𝑷∧∀w∈B¬v<𝑷w∧y∈A→C+𝑹v1𝑷~𝑹<𝑹y→¬C+𝑹v1𝑷~𝑹<𝑹y
85 84 pm2.01d ⊢v∈𝑷∧∀w∈B¬v<𝑷w∧y∈A→¬C+𝑹v1𝑷~𝑹<𝑹y
86 85 expr ⊢v∈𝑷∧∀w∈B¬v<𝑷w→y∈A→¬C+𝑹v1𝑷~𝑹<𝑹y
87 86 ralrimiv ⊢v∈𝑷∧∀w∈B¬v<𝑷w→∀y∈A¬C+𝑹v1𝑷~𝑹<𝑹y
88 87 ex ⊢v∈𝑷→∀w∈B¬v<𝑷w→∀y∈A¬C+𝑹v1𝑷~𝑹<𝑹y
89 88 adantl ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x∧v∈𝑷→∀w∈B¬v<𝑷w→∀y∈A¬C+𝑹v1𝑷~𝑹<𝑹y
90 r19.29 ⊢∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u∧∃w∈𝑷C+𝑹w1𝑷~𝑹=y→∃w∈𝑷w<𝑷v→∃u∈Bw<𝑷u∧C+𝑹w1𝑷~𝑹=y
91 breq1 ⊢C+𝑹w1𝑷~𝑹=y→C+𝑹w1𝑷~𝑹<𝑹C+𝑹v1𝑷~𝑹↔y<𝑹C+𝑹v1𝑷~𝑹
92 46 91 bitr3id ⊢C+𝑹w1𝑷~𝑹=y→w<𝑷v↔y<𝑹C+𝑹v1𝑷~𝑹
93 92 biimprd ⊢C+𝑹w1𝑷~𝑹=y→y<𝑹C+𝑹v1𝑷~𝑹→w<𝑷v
94 vex ⊢u∈V
95 opeq1 ⊢w=u→w1𝑷=u1𝑷
96 95 eceq1d ⊢w=u→w1𝑷~𝑹=u1𝑷~𝑹
97 96 oveq2d ⊢w=u→C+𝑹w1𝑷~𝑹=C+𝑹u1𝑷~𝑹
98 97 eleq1d ⊢w=u→C+𝑹w1𝑷~𝑹∈A↔C+𝑹u1𝑷~𝑹∈A
99 94 98 1 elab2 ⊢u∈B↔C+𝑹u1𝑷~𝑹∈A
100 breq2 ⊢z=C+𝑹u1𝑷~𝑹→C+𝑹w1𝑷~𝑹<𝑹z↔C+𝑹w1𝑷~𝑹<𝑹C+𝑹u1𝑷~𝑹
101 2 ltpsrpr ⊢C+𝑹w1𝑷~𝑹<𝑹C+𝑹u1𝑷~𝑹↔w<𝑷u
102 100 101 bitrdi ⊢z=C+𝑹u1𝑷~𝑹→C+𝑹w1𝑷~𝑹<𝑹z↔w<𝑷u
103 102 rspcev ⊢C+𝑹u1𝑷~𝑹∈A∧w<𝑷u→∃z∈AC+𝑹w1𝑷~𝑹<𝑹z
104 99 103 sylanb ⊢u∈B∧w<𝑷u→∃z∈AC+𝑹w1𝑷~𝑹<𝑹z
105 104 rexlimiva ⊢∃u∈Bw<𝑷u→∃z∈AC+𝑹w1𝑷~𝑹<𝑹z
106 breq1 ⊢C+𝑹w1𝑷~𝑹=y→C+𝑹w1𝑷~𝑹<𝑹z↔y<𝑹z
107 106 rexbidv ⊢C+𝑹w1𝑷~𝑹=y→∃z∈AC+𝑹w1𝑷~𝑹<𝑹z↔∃z∈Ay<𝑹z
108 105 107 imbitrid ⊢C+𝑹w1𝑷~𝑹=y→∃u∈Bw<𝑷u→∃z∈Ay<𝑹z
109 93 108 imim12d ⊢C+𝑹w1𝑷~𝑹=y→w<𝑷v→∃u∈Bw<𝑷u→y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
110 109 impcom ⊢w<𝑷v→∃u∈Bw<𝑷u∧C+𝑹w1𝑷~𝑹=y→y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
111 110 rexlimivw ⊢∃w∈𝑷w<𝑷v→∃u∈Bw<𝑷u∧C+𝑹w1𝑷~𝑹=y→y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
112 90 111 syl ⊢∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u∧∃w∈𝑷C+𝑹w1𝑷~𝑹=y→y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
113 65 112 sylan2b ⊢∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u∧C+𝑹-1𝑹<𝑹y→y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
114 113 ex ⊢∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u→C+𝑹-1𝑹<𝑹y→y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
115 114 adantl ⊢C∈A∧v∈𝑷∧∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u→C+𝑹-1𝑹<𝑹y→y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
116 115 a1dd ⊢C∈A∧v∈𝑷∧∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u→C+𝑹-1𝑹<𝑹y→y∈𝑹→y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
117 34 35 sotri2 ⊢y∈𝑹∧¬C+𝑹-1𝑹<𝑹y∧C+𝑹-1𝑹<𝑹C→y<𝑹C
118 33 117 mp3an3 ⊢y∈𝑹∧¬C+𝑹-1𝑹<𝑹y→y<𝑹C
119 breq2 ⊢z=C→y<𝑹z↔y<𝑹C
120 119 rspcev ⊢C∈A∧y<𝑹C→∃z∈Ay<𝑹z
121 120 ex ⊢C∈A→y<𝑹C→∃z∈Ay<𝑹z
122 121 a1dd ⊢C∈A→y<𝑹C→y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
123 118 122 syl5 ⊢C∈A→y∈𝑹∧¬C+𝑹-1𝑹<𝑹y→y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
124 123 expcomd ⊢C∈A→¬C+𝑹-1𝑹<𝑹y→y∈𝑹→y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
125 124 ad2antrr ⊢C∈A∧v∈𝑷∧∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u→¬C+𝑹-1𝑹<𝑹y→y∈𝑹→y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
126 116 125 pm2.61d ⊢C∈A∧v∈𝑷∧∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u→y∈𝑹→y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
127 126 ralrimiv ⊢C∈A∧v∈𝑷∧∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u→∀y∈𝑹y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
128 127 ex ⊢C∈A∧v∈𝑷→∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u→∀y∈𝑹y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
129 128 adantlr ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x∧v∈𝑷→∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u→∀y∈𝑹y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
130 89 129 anim12d ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x∧v∈𝑷→∀w∈B¬v<𝑷w∧∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u→∀y∈A¬C+𝑹v1𝑷~𝑹<𝑹y∧∀y∈𝑹y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
131 breq1 ⊢x=C+𝑹v1𝑷~𝑹→x<𝑹y↔C+𝑹v1𝑷~𝑹<𝑹y
132 131 notbid ⊢x=C+𝑹v1𝑷~𝑹→¬x<𝑹y↔¬C+𝑹v1𝑷~𝑹<𝑹y
133 132 ralbidv ⊢x=C+𝑹v1𝑷~𝑹→∀y∈A¬x<𝑹y↔∀y∈A¬C+𝑹v1𝑷~𝑹<𝑹y
134 breq2 ⊢x=C+𝑹v1𝑷~𝑹→y<𝑹x↔y<𝑹C+𝑹v1𝑷~𝑹
135 134 imbi1d ⊢x=C+𝑹v1𝑷~𝑹→y<𝑹x→∃z∈Ay<𝑹z↔y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
136 135 ralbidv ⊢x=C+𝑹v1𝑷~𝑹→∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z↔∀y∈𝑹y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
137 133 136 anbi12d ⊢x=C+𝑹v1𝑷~𝑹→∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z↔∀y∈A¬C+𝑹v1𝑷~𝑹<𝑹y∧∀y∈𝑹y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z
138 137 rspcev ⊢C+𝑹v1𝑷~𝑹∈𝑹∧∀y∈A¬C+𝑹v1𝑷~𝑹<𝑹y∧∀y∈𝑹y<𝑹C+𝑹v1𝑷~𝑹→∃z∈Ay<𝑹z→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z
139 62 130 138 syl6an ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x∧v∈𝑷→∀w∈B¬v<𝑷w∧∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z
140 139 rexlimdva ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x→∃v∈𝑷∀w∈B¬v<𝑷w∧∀w∈𝑷w<𝑷v→∃u∈Bw<𝑷u→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z
141 57 140 mpd ⊢C∈A∧∃x∈𝑹∀y∈Ay<𝑹x→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z