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 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) )