Metamath Proof Explorer

Theorem coflton

Description: Cofinality theorem for ordinals. If A is cofinal with B and B precedes C , then A precedes C . Compare cofsslt for surreals. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Hypotheses coflton.1 ⊢ φ → A ⊆ On
coflton.2 ⊢ φ → B ⊆ On
coflton.3 ⊢ φ → C ⊆ On
coflton.4 ⊢ φ → ∀ x ∈ A ∃ y ∈ B x ⊆ y
coflton.5 ⊢ φ → ∀ z ∈ B ∀ w ∈ C z ∈ w
Assertion coflton ⊢ φ → ∀ a ∈ A ∀ c ∈ C a ∈ c

Proof

Step Hyp Ref Expression
1 coflton.1 ⊢ φ → A ⊆ On
2 coflton.2 ⊢ φ → B ⊆ On
3 coflton.3 ⊢ φ → C ⊆ On
4 coflton.4 ⊢ φ → ∀ x ∈ A ∃ y ∈ B x ⊆ y
5 coflton.5 ⊢ φ → ∀ z ∈ B ∀ w ∈ C z ∈ w
6 sseq1 ⊢ x = a → x ⊆ y ↔ a ⊆ y
7 6 rexbidv ⊢ x = a → ∃ y ∈ B x ⊆ y ↔ ∃ y ∈ B a ⊆ y
8 4 adantr ⊢ φ ∧ a ∈ A → ∀ x ∈ A ∃ y ∈ B x ⊆ y
9 simpr ⊢ φ ∧ a ∈ A → a ∈ A
10 7 8 9 rspcdva ⊢ φ ∧ a ∈ A → ∃ y ∈ B a ⊆ y
11 10 adantrr ⊢ φ ∧ a ∈ A ∧ c ∈ C → ∃ y ∈ B a ⊆ y
12 sseq2 ⊢ y = b → a ⊆ y ↔ a ⊆ b
13 12 cbvrexvw ⊢ ∃ y ∈ B a ⊆ y ↔ ∃ b ∈ B a ⊆ b
14 11 13 sylib ⊢ φ ∧ a ∈ A ∧ c ∈ C → ∃ b ∈ B a ⊆ b
15 simpr ⊢ φ ∧ a ∈ A ∧ c ∈ C ∧ b ∈ B → b ∈ B
16 simplrr ⊢ φ ∧ a ∈ A ∧ c ∈ C ∧ b ∈ B → c ∈ C
17 5 ad2antrr ⊢ φ ∧ a ∈ A ∧ c ∈ C ∧ b ∈ B → ∀ z ∈ B ∀ w ∈ C z ∈ w
18 elequ1 ⊢ z = b → z ∈ w ↔ b ∈ w
19 elequ2 ⊢ w = c → b ∈ w ↔ b ∈ c
20 18 19 rspc2va ⊢ b ∈ B ∧ c ∈ C ∧ ∀ z ∈ B ∀ w ∈ C z ∈ w → b ∈ c
21 15 16 17 20 syl21anc ⊢ φ ∧ a ∈ A ∧ c ∈ C ∧ b ∈ B → b ∈ c
22 1 sselda ⊢ φ ∧ a ∈ A → a ∈ On
23 22 adantrr ⊢ φ ∧ a ∈ A ∧ c ∈ C → a ∈ On
24 3 sselda ⊢ φ ∧ c ∈ C → c ∈ On
25 24 adantrl ⊢ φ ∧ a ∈ A ∧ c ∈ C → c ∈ On
26 25 adantr ⊢ φ ∧ a ∈ A ∧ c ∈ C ∧ b ∈ B → c ∈ On
27 ontr2 ⊢ a ∈ On ∧ c ∈ On → a ⊆ b ∧ b ∈ c → a ∈ c
28 23 26 27 syl2an2r ⊢ φ ∧ a ∈ A ∧ c ∈ C ∧ b ∈ B → a ⊆ b ∧ b ∈ c → a ∈ c
29 21 28 mpan2d ⊢ φ ∧ a ∈ A ∧ c ∈ C ∧ b ∈ B → a ⊆ b → a ∈ c
30 29 rexlimdva ⊢ φ ∧ a ∈ A ∧ c ∈ C → ∃ b ∈ B a ⊆ b → a ∈ c
31 14 30 mpd ⊢ φ ∧ a ∈ A ∧ c ∈ C → a ∈ c
32 31 ralrimivva ⊢ φ → ∀ a ∈ A ∀ c ∈ C a ∈ c