Metamath Proof Explorer

Theorem cofsslt

Description: If every element of A is bounded above by some element of B and B precedes C , then A precedes C . Note - we will often use the term "cofinal" to denote that every element of A is bounded above by some element of B . Similarly, we will use the term "coinitial" to denote that every element of A is bounded below by some element of B . (Contributed by Scott Fenton, 24-Sep-2024)

Ref Expression
Assertion cofsslt ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) → 𝐴 <<s 𝐶 )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) → 𝐴 ∈ 𝒫 No )
2 ssltex2 ⊢ ( 𝐵 <<s 𝐶 → 𝐶 ∈ V )
3 2 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) → 𝐶 ∈ V )
4 1 elpwid ⊢ ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) → 𝐴 ⊆ No )
5 ssltss2 ⊢ ( 𝐵 <<s 𝐶 → 𝐶 ⊆ No )
6 5 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) → 𝐶 ⊆ No )
7 breq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ≤s 𝑦 ↔ 𝑎 ≤s 𝑦 ) )
8 7 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ↔ ∃ 𝑦 ∈ 𝐵 𝑎 ≤s 𝑦 ) )
9 simp12 ⊢ ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 )
10 simp2 ⊢ ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) → 𝑎 ∈ 𝐴 )
11 8 9 10 rspcdva ⊢ ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) → ∃ 𝑦 ∈ 𝐵 𝑎 ≤s 𝑦 )
12 breq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑎 ≤s 𝑦 ↔ 𝑎 ≤s 𝑏 ) )
13 12 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐵 𝑎 ≤s 𝑦 ↔ ∃ 𝑏 ∈ 𝐵 𝑎 ≤s 𝑏 )
14 11 13 sylib ⊢ ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) → ∃ 𝑏 ∈ 𝐵 𝑎 ≤s 𝑏 )
15 simpl11 ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝐴 ∈ 𝒫 No )
16 15 elpwid ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝐴 ⊆ No )
17 simpl2 ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝑎 ∈ 𝐴 )
18 16 17 sseldd ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝑎 ∈ No )
19 simpl13 ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝐵 <<s 𝐶 )
20 ssltss1 ⊢ ( 𝐵 <<s 𝐶 → 𝐵 ⊆ No )
21 19 20 syl ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝐵 ⊆ No )
22 simprl ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝑏 ∈ 𝐵 )
23 21 22 sseldd ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝑏 ∈ No )
24 19 5 syl ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝐶 ⊆ No )
25 simpl3 ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝑐 ∈ 𝐶 )
26 24 25 sseldd ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝑐 ∈ No )
27 simprr ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝑎 ≤s 𝑏 )
28 19 22 25 ssltsepcd ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝑏 <s 𝑐 )
29 18 23 26 27 28 slelttrd ⊢ ( ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ≤s 𝑏 ) ) → 𝑎 <s 𝑐 )
30 14 29 rexlimddv ⊢ ( ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) → 𝑎 <s 𝑐 )
31 1 3 4 6 30 ssltd ⊢ ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶 ) → 𝐴 <<s 𝐶 )