This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sorpss

Description: Express strict ordering under proper subsets, i.e. the notion of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion sorpss ( [⊊] Or 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 porpss ⊢ [⊊] Po 𝐴
2 1 biantrur ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 [⊊] 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 [⊊] 𝑥 ) ↔ ( [⊊] Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 [⊊] 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 [⊊] 𝑥 ) ) )
3 sspsstri ⊢ ( ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) ↔ ( 𝑥 ⊊ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ⊊ 𝑥 ) )
4 vex ⊢ 𝑦 ∈ V
5 4 brrpss ⊢ ( 𝑥 [⊊] 𝑦 ↔ 𝑥 ⊊ 𝑦 )
6 biid ⊢ ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑦 )
7 vex ⊢ 𝑥 ∈ V
8 7 brrpss ⊢ ( 𝑦 [⊊] 𝑥 ↔ 𝑦 ⊊ 𝑥 )
9 5 6 8 3orbi123i ⊢ ( ( 𝑥 [⊊] 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 [⊊] 𝑥 ) ↔ ( 𝑥 ⊊ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ⊊ 𝑥 ) )
10 3 9 bitr4i ⊢ ( ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) ↔ ( 𝑥 [⊊] 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 [⊊] 𝑥 ) )
11 10 2ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 [⊊] 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 [⊊] 𝑥 ) )
12 df-so ⊢ ( [⊊] Or 𝐴 ↔ ( [⊊] Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 [⊊] 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 [⊊] 𝑥 ) ) )
13 2 11 12 3bitr4ri ⊢ ( [⊊] Or 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) )