Theorem porpss

Description: Every class is partially ordered by proper subsets. (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Assertion	porpss	⊢ [⊊] Po 𝐴

Proof

Step	Hyp	Ref	Expression
1		pssirr	⊢ ¬ 𝑥 ⊊ 𝑥
2		psstr	⊢ ( ( 𝑥 ⊊ 𝑦 ∧ 𝑦 ⊊ 𝑧 ) → 𝑥 ⊊ 𝑧 )
3		vex	⊢ 𝑥 ∈ V
4	3	brrpss	⊢ ( 𝑥 [⊊] 𝑥 ↔ 𝑥 ⊊ 𝑥 )
5	4	notbii	⊢ ( ¬ 𝑥 [⊊] 𝑥 ↔ ¬ 𝑥 ⊊ 𝑥 )
6		vex	⊢ 𝑦 ∈ V
7	6	brrpss	⊢ ( 𝑥 [⊊] 𝑦 ↔ 𝑥 ⊊ 𝑦 )
8		vex	⊢ 𝑧 ∈ V
9	8	brrpss	⊢ ( 𝑦 [⊊] 𝑧 ↔ 𝑦 ⊊ 𝑧 )
10	7 9	anbi12i	⊢ ( ( 𝑥 [⊊] 𝑦 ∧ 𝑦 [⊊] 𝑧 ) ↔ ( 𝑥 ⊊ 𝑦 ∧ 𝑦 ⊊ 𝑧 ) )
11	8	brrpss	⊢ ( 𝑥 [⊊] 𝑧 ↔ 𝑥 ⊊ 𝑧 )
12	10 11	imbi12i	⊢ ( ( ( 𝑥 [⊊] 𝑦 ∧ 𝑦 [⊊] 𝑧 ) → 𝑥 [⊊] 𝑧 ) ↔ ( ( 𝑥 ⊊ 𝑦 ∧ 𝑦 ⊊ 𝑧 ) → 𝑥 ⊊ 𝑧 ) )
13	5 12	anbi12i	⊢ ( ( ¬ 𝑥 [⊊] 𝑥 ∧ ( ( 𝑥 [⊊] 𝑦 ∧ 𝑦 [⊊] 𝑧 ) → 𝑥 [⊊] 𝑧 ) ) ↔ ( ¬ 𝑥 ⊊ 𝑥 ∧ ( ( 𝑥 ⊊ 𝑦 ∧ 𝑦 ⊊ 𝑧 ) → 𝑥 ⊊ 𝑧 ) ) )
14	1 2 13	mpbir2an	⊢ ( ¬ 𝑥 [⊊] 𝑥 ∧ ( ( 𝑥 [⊊] 𝑦 ∧ 𝑦 [⊊] 𝑧 ) → 𝑥 [⊊] 𝑧 ) )
15	14	rgenw	⊢ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 [⊊] 𝑥 ∧ ( ( 𝑥 [⊊] 𝑦 ∧ 𝑦 [⊊] 𝑧 ) → 𝑥 [⊊] 𝑧 ) )
16	15	rgen2w	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 [⊊] 𝑥 ∧ ( ( 𝑥 [⊊] 𝑦 ∧ 𝑦 [⊊] 𝑧 ) → 𝑥 [⊊] 𝑧 ) )
17		df-po	⊢ ( [⊊] Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 [⊊] 𝑥 ∧ ( ( 𝑥 [⊊] 𝑦 ∧ 𝑦 [⊊] 𝑧 ) → 𝑥 [⊊] 𝑧 ) ) )
18	16 17	mpbir	⊢ [⊊] Po 𝐴