Metamath Proof Explorer

Theorem coinitsslt

Description: If B is coinitial with C and A precedes C , then A precedes B . (Contributed by Scott Fenton, 24-Sep-2024)

Ref Expression
Assertion coinitsslt ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC→A≪sB

Proof

Step Hyp Ref Expression
1 ssltex1 ⊢A≪sC→A∈V
2 1 3ad2ant3 ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC→A∈V
3 simp1 ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC→B∈𝒫No
4 ssltss1 ⊢A≪sC→A⊆No
5 4 3ad2ant3 ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC→A⊆No
6 3 elpwid ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC→B⊆No
7 breq2 ⊢x=b→y≤sx↔y≤sb
8 7 rexbidv ⊢x=b→∃y∈Cy≤sx↔∃y∈Cy≤sb
9 simp12 ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B→∀x∈B∃y∈Cy≤sx
10 simp3 ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B→b∈B
11 8 9 10 rspcdva ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B→∃y∈Cy≤sb
12 breq1 ⊢y=c→y≤sb↔c≤sb
13 12 cbvrexvw ⊢∃y∈Cy≤sb↔∃c∈Cc≤sb
14 11 13 sylib ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B→∃c∈Cc≤sb
15 simpl13 ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→A≪sC
16 15 4 syl ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→A⊆No
17 simpl2 ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→a∈A
18 16 17 sseldd ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→a∈No
19 ssltss2 ⊢A≪sC→C⊆No
20 15 19 syl ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→C⊆No
21 simprl ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→c∈C
22 20 21 sseldd ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→c∈No
23 simpl1 ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC
24 23 6 syl ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→B⊆No
25 simpl3 ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→b∈B
26 24 25 sseldd ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→b∈No
27 15 17 21 ssltsepcd ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→a<sc
28 simprr ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→c≤sb
29 18 22 26 27 28 sltletrd ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B∧c∈C∧c≤sb→a<sb
30 14 29 rexlimddv ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC∧a∈A∧b∈B→a<sb
31 2 3 5 6 30 ssltd ⊢B∈𝒫No∧∀x∈B∃y∈Cy≤sx∧A≪sC→A≪sB