Metamath Proof Explorer

Theorem ltsopr

Description: Positive real 'less than' is a strict ordering. Part of Proposition 9-3.3 of Gleason p. 122. (Contributed by NM, 25-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion ltsopr ${⊢}{<}_{𝑷}\mathrm{Or}𝑷$

Proof

Step Hyp Ref Expression
1 pssirr ${⊢}¬{x}\subset {x}$
2 ltprord ${⊢}\left({x}\in 𝑷\wedge {x}\in 𝑷\right)\to \left({x}{<}_{𝑷}{x}↔{x}\subset {x}\right)$
3 1 2 mtbiri ${⊢}\left({x}\in 𝑷\wedge {x}\in 𝑷\right)\to ¬{x}{<}_{𝑷}{x}$
4 3 anidms ${⊢}{x}\in 𝑷\to ¬{x}{<}_{𝑷}{x}$
5 psstr ${⊢}\left({x}\subset {y}\wedge {y}\subset {z}\right)\to {x}\subset {z}$
6 ltprord ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\to \left({x}{<}_{𝑷}{y}↔{x}\subset {y}\right)$
7 6 3adant3 ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\wedge {z}\in 𝑷\right)\to \left({x}{<}_{𝑷}{y}↔{x}\subset {y}\right)$
8 ltprord ${⊢}\left({y}\in 𝑷\wedge {z}\in 𝑷\right)\to \left({y}{<}_{𝑷}{z}↔{y}\subset {z}\right)$
9 8 3adant1 ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\wedge {z}\in 𝑷\right)\to \left({y}{<}_{𝑷}{z}↔{y}\subset {z}\right)$
10 7 9 anbi12d ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\wedge {z}\in 𝑷\right)\to \left(\left({x}{<}_{𝑷}{y}\wedge {y}{<}_{𝑷}{z}\right)↔\left({x}\subset {y}\wedge {y}\subset {z}\right)\right)$
11 ltprord ${⊢}\left({x}\in 𝑷\wedge {z}\in 𝑷\right)\to \left({x}{<}_{𝑷}{z}↔{x}\subset {z}\right)$
12 11 3adant2 ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\wedge {z}\in 𝑷\right)\to \left({x}{<}_{𝑷}{z}↔{x}\subset {z}\right)$
13 10 12 imbi12d ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\wedge {z}\in 𝑷\right)\to \left(\left(\left({x}{<}_{𝑷}{y}\wedge {y}{<}_{𝑷}{z}\right)\to {x}{<}_{𝑷}{z}\right)↔\left(\left({x}\subset {y}\wedge {y}\subset {z}\right)\to {x}\subset {z}\right)\right)$
14 5 13 mpbiri ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\wedge {z}\in 𝑷\right)\to \left(\left({x}{<}_{𝑷}{y}\wedge {y}{<}_{𝑷}{z}\right)\to {x}{<}_{𝑷}{z}\right)$
15 psslinpr ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\to \left({x}\subset {y}\vee {x}={y}\vee {y}\subset {x}\right)$
16 biidd ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\to \left({x}={y}↔{x}={y}\right)$
17 ltprord ${⊢}\left({y}\in 𝑷\wedge {x}\in 𝑷\right)\to \left({y}{<}_{𝑷}{x}↔{y}\subset {x}\right)$
18 17 ancoms ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\to \left({y}{<}_{𝑷}{x}↔{y}\subset {x}\right)$
19 6 16 18 3orbi123d ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\to \left(\left({x}{<}_{𝑷}{y}\vee {x}={y}\vee {y}{<}_{𝑷}{x}\right)↔\left({x}\subset {y}\vee {x}={y}\vee {y}\subset {x}\right)\right)$
20 15 19 mpbird ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\to \left({x}{<}_{𝑷}{y}\vee {x}={y}\vee {y}{<}_{𝑷}{x}\right)$
21 4 14 20 issoi ${⊢}{<}_{𝑷}\mathrm{Or}𝑷$