# Metamath Proof Explorer

## Theorem coflim

Description: A simpler expression for the cofinality predicate, at a limit ordinal. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion coflim ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\right)\to \left(\bigcup {B}={A}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)$

### Proof

Step Hyp Ref Expression
1 eleq2 ${⊢}\bigcup {B}={A}\to \left({x}\in \bigcup {B}↔{x}\in {A}\right)$
2 1 biimprd ${⊢}\bigcup {B}={A}\to \left({x}\in {A}\to {x}\in \bigcup {B}\right)$
3 eluni2 ${⊢}{x}\in \bigcup {B}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\in {y}$
4 limord ${⊢}\mathrm{Lim}{A}\to \mathrm{Ord}{A}$
5 ssel2 ${⊢}\left({B}\subseteq {A}\wedge {y}\in {B}\right)\to {y}\in {A}$
6 ordelon ${⊢}\left(\mathrm{Ord}{A}\wedge {y}\in {A}\right)\to {y}\in \mathrm{On}$
7 4 5 6 syl2an ${⊢}\left(\mathrm{Lim}{A}\wedge \left({B}\subseteq {A}\wedge {y}\in {B}\right)\right)\to {y}\in \mathrm{On}$
8 7 expr ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\right)\to \left({y}\in {B}\to {y}\in \mathrm{On}\right)$
9 onelss ${⊢}{y}\in \mathrm{On}\to \left({x}\in {y}\to {x}\subseteq {y}\right)$
10 8 9 syl6 ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\right)\to \left({y}\in {B}\to \left({x}\in {y}\to {x}\subseteq {y}\right)\right)$
11 10 reximdvai ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\right)\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)$
12 3 11 syl5bi ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\right)\to \left({x}\in \bigcup {B}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)$
13 2 12 syl9r ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\right)\to \left(\bigcup {B}={A}\to \left({x}\in {A}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\right)$
14 13 ralrimdv ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\right)\to \left(\bigcup {B}={A}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)$
15 uniss ${⊢}{B}\subseteq {A}\to \bigcup {B}\subseteq \bigcup {A}$
16 15 3ad2ant2 ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\to \bigcup {B}\subseteq \bigcup {A}$
17 uniss2 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\to \bigcup {A}\subseteq \bigcup {B}$
18 17 3ad2ant3 ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\to \bigcup {A}\subseteq \bigcup {B}$
19 16 18 eqssd ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\to \bigcup {B}=\bigcup {A}$
20 limuni ${⊢}\mathrm{Lim}{A}\to {A}=\bigcup {A}$
21 20 3ad2ant1 ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\to {A}=\bigcup {A}$
22 19 21 eqtr4d ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)\to \bigcup {B}={A}$
23 22 3expia ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\to \bigcup {B}={A}\right)$
24 14 23 impbid ${⊢}\left(\mathrm{Lim}{A}\wedge {B}\subseteq {A}\right)\to \left(\bigcup {B}={A}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)$