Metamath Proof Explorer

Theorem onint

Description: The intersection (infimum) of a nonempty class of ordinal numbers belongs to the class. Compare Exercise 4 of TakeutiZaring p. 45. (Contributed by NM, 31-Jan-1997)

Ref Expression
Assertion onint ${⊢}\left({A}\subseteq \mathrm{On}\wedge {A}\ne \varnothing \right)\to \bigcap {A}\in {A}$

Proof

Step Hyp Ref Expression
1 ordon ${⊢}\mathrm{Ord}\mathrm{On}$
2 tz7.5 ${⊢}\left(\mathrm{Ord}\mathrm{On}\wedge {A}\subseteq \mathrm{On}\wedge {A}\ne \varnothing \right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{A}\cap {x}=\varnothing$
3 1 2 mp3an1 ${⊢}\left({A}\subseteq \mathrm{On}\wedge {A}\ne \varnothing \right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{A}\cap {x}=\varnothing$
4 ssel ${⊢}{A}\subseteq \mathrm{On}\to \left({x}\in {A}\to {x}\in \mathrm{On}\right)$
5 4 imdistani ${⊢}\left({A}\subseteq \mathrm{On}\wedge {x}\in {A}\right)\to \left({A}\subseteq \mathrm{On}\wedge {x}\in \mathrm{On}\right)$
6 ssel ${⊢}{A}\subseteq \mathrm{On}\to \left({z}\in {A}\to {z}\in \mathrm{On}\right)$
7 ontri1 ${⊢}\left({x}\in \mathrm{On}\wedge {z}\in \mathrm{On}\right)\to \left({x}\subseteq {z}↔¬{z}\in {x}\right)$
8 ssel ${⊢}{x}\subseteq {z}\to \left({y}\in {x}\to {y}\in {z}\right)$
9 7 8 syl6bir ${⊢}\left({x}\in \mathrm{On}\wedge {z}\in \mathrm{On}\right)\to \left(¬{z}\in {x}\to \left({y}\in {x}\to {y}\in {z}\right)\right)$
10 9 ex ${⊢}{x}\in \mathrm{On}\to \left({z}\in \mathrm{On}\to \left(¬{z}\in {x}\to \left({y}\in {x}\to {y}\in {z}\right)\right)\right)$
11 6 10 sylan9 ${⊢}\left({A}\subseteq \mathrm{On}\wedge {x}\in \mathrm{On}\right)\to \left({z}\in {A}\to \left(¬{z}\in {x}\to \left({y}\in {x}\to {y}\in {z}\right)\right)\right)$
12 11 com4r ${⊢}{y}\in {x}\to \left(\left({A}\subseteq \mathrm{On}\wedge {x}\in \mathrm{On}\right)\to \left({z}\in {A}\to \left(¬{z}\in {x}\to {y}\in {z}\right)\right)\right)$
13 12 imp31 ${⊢}\left(\left({y}\in {x}\wedge \left({A}\subseteq \mathrm{On}\wedge {x}\in \mathrm{On}\right)\right)\wedge {z}\in {A}\right)\to \left(¬{z}\in {x}\to {y}\in {z}\right)$
14 13 ralimdva ${⊢}\left({y}\in {x}\wedge \left({A}\subseteq \mathrm{On}\wedge {x}\in \mathrm{On}\right)\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}¬{z}\in {x}\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {z}\right)$
15 disj ${⊢}{A}\cap {x}=\varnothing ↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}¬{z}\in {x}$
16 vex ${⊢}{y}\in \mathrm{V}$
17 16 elint2 ${⊢}{y}\in \bigcap {A}↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {z}$
18 14 15 17 3imtr4g ${⊢}\left({y}\in {x}\wedge \left({A}\subseteq \mathrm{On}\wedge {x}\in \mathrm{On}\right)\right)\to \left({A}\cap {x}=\varnothing \to {y}\in \bigcap {A}\right)$
19 5 18 sylan2 ${⊢}\left({y}\in {x}\wedge \left({A}\subseteq \mathrm{On}\wedge {x}\in {A}\right)\right)\to \left({A}\cap {x}=\varnothing \to {y}\in \bigcap {A}\right)$
20 19 exp32 ${⊢}{y}\in {x}\to \left({A}\subseteq \mathrm{On}\to \left({x}\in {A}\to \left({A}\cap {x}=\varnothing \to {y}\in \bigcap {A}\right)\right)\right)$
21 20 com4l ${⊢}{A}\subseteq \mathrm{On}\to \left({x}\in {A}\to \left({A}\cap {x}=\varnothing \to \left({y}\in {x}\to {y}\in \bigcap {A}\right)\right)\right)$
22 21 imp32 ${⊢}\left({A}\subseteq \mathrm{On}\wedge \left({x}\in {A}\wedge {A}\cap {x}=\varnothing \right)\right)\to \left({y}\in {x}\to {y}\in \bigcap {A}\right)$
23 22 ssrdv ${⊢}\left({A}\subseteq \mathrm{On}\wedge \left({x}\in {A}\wedge {A}\cap {x}=\varnothing \right)\right)\to {x}\subseteq \bigcap {A}$
24 intss1 ${⊢}{x}\in {A}\to \bigcap {A}\subseteq {x}$
25 24 ad2antrl ${⊢}\left({A}\subseteq \mathrm{On}\wedge \left({x}\in {A}\wedge {A}\cap {x}=\varnothing \right)\right)\to \bigcap {A}\subseteq {x}$
26 23 25 eqssd ${⊢}\left({A}\subseteq \mathrm{On}\wedge \left({x}\in {A}\wedge {A}\cap {x}=\varnothing \right)\right)\to {x}=\bigcap {A}$
27 26 eleq1d ${⊢}\left({A}\subseteq \mathrm{On}\wedge \left({x}\in {A}\wedge {A}\cap {x}=\varnothing \right)\right)\to \left({x}\in {A}↔\bigcap {A}\in {A}\right)$
28 27 biimpd ${⊢}\left({A}\subseteq \mathrm{On}\wedge \left({x}\in {A}\wedge {A}\cap {x}=\varnothing \right)\right)\to \left({x}\in {A}\to \bigcap {A}\in {A}\right)$
29 28 exp32 ${⊢}{A}\subseteq \mathrm{On}\to \left({x}\in {A}\to \left({A}\cap {x}=\varnothing \to \left({x}\in {A}\to \bigcap {A}\in {A}\right)\right)\right)$
30 29 com34 ${⊢}{A}\subseteq \mathrm{On}\to \left({x}\in {A}\to \left({x}\in {A}\to \left({A}\cap {x}=\varnothing \to \bigcap {A}\in {A}\right)\right)\right)$
31 30 pm2.43d ${⊢}{A}\subseteq \mathrm{On}\to \left({x}\in {A}\to \left({A}\cap {x}=\varnothing \to \bigcap {A}\in {A}\right)\right)$
32 31 rexlimdv ${⊢}{A}\subseteq \mathrm{On}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{A}\cap {x}=\varnothing \to \bigcap {A}\in {A}\right)$
33 3 32 syl5 ${⊢}{A}\subseteq \mathrm{On}\to \left(\left({A}\subseteq \mathrm{On}\wedge {A}\ne \varnothing \right)\to \bigcap {A}\in {A}\right)$
34 33 anabsi5 ${⊢}\left({A}\subseteq \mathrm{On}\wedge {A}\ne \varnothing \right)\to \bigcap {A}\in {A}$