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

Metamath Proof Explorer

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 𝐴