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 ⊢ ( 𝜑 → 𝐴 ⊆ On )
coflton.2 ⊢ ( 𝜑 → 𝐵 ⊆ On )
coflton.3 ⊢ ( 𝜑 → 𝐶 ⊆ On )
coflton.4 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 )
coflton.5 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝑧 ∈ 𝑤 )
Assertion coflton ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ∀ 𝑐 ∈ 𝐶 𝑎 ∈ 𝑐 )

Proof

Step Hyp Ref Expression
1 coflton.1 ⊢ ( 𝜑 → 𝐴 ⊆ On )
2 coflton.2 ⊢ ( 𝜑 → 𝐵 ⊆ On )
3 coflton.3 ⊢ ( 𝜑 → 𝐶 ⊆ On )
4 coflton.4 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 )
5 coflton.5 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝑧 ∈ 𝑤 )
6 sseq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑦 ) )
7 6 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ↔ ∃ 𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦 ) )
8 4 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
10 7 8 9 rspcdva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦 )
11 10 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ) → ∃ 𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦 )
12 sseq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑎 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑏 ) )
13 12 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦 ↔ ∃ 𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 )
14 11 13 sylib ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ) → ∃ 𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 )
15 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
16 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑐 ∈ 𝐶 )
17 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ) ∧ 𝑏 ∈ 𝐵 ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝑧 ∈ 𝑤 )
18 elequ1 ⊢ ( 𝑧 = 𝑏 → ( 𝑧 ∈ 𝑤 ↔ 𝑏 ∈ 𝑤 ) )
19 elequ2 ⊢ ( 𝑤 = 𝑐 → ( 𝑏 ∈ 𝑤 ↔ 𝑏 ∈ 𝑐 ) )
20 18 19 rspc2va ⊢ ( ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝑧 ∈ 𝑤 ) → 𝑏 ∈ 𝑐 )
21 15 16 17 20 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝑐 )
22 1 sselda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ On )
23 22 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑎 ∈ On )
24 3 sselda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑐 ∈ On )
25 24 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑐 ∈ On )
26 25 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑐 ∈ On )
27 ontr2 ⊢ ( ( 𝑎 ∈ On ∧ 𝑐 ∈ On ) → ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ∈ 𝑐 ) → 𝑎 ∈ 𝑐 ) )
28 23 26 27 syl2an2r ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ∈ 𝑐 ) → 𝑎 ∈ 𝑐 ) )
29 21 28 mpan2d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ⊆ 𝑏 → 𝑎 ∈ 𝑐 ) )
30 29 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∃ 𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 → 𝑎 ∈ 𝑐 ) )
31 14 30 mpd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑎 ∈ 𝑐 )
32 31 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ∀ 𝑐 ∈ 𝐶 𝑎 ∈ 𝑐 )