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

Metamath Proof Explorer

Theorem posn

Description: Partial ordering of a singleton. (Contributed by NM, 27-Apr-2009) (Revised by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion posn ( Rel 𝑅 → ( 𝑅 Po { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )

Proof

Step Hyp Ref Expression
1 po0 ⊢ 𝑅 Po ∅
2 snprc ⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
3 poeq2 ⊢ ( { 𝐴 } = ∅ → ( 𝑅 Po { 𝐴 } ↔ 𝑅 Po ∅ ) )
4 2 3 sylbi ⊢ ( ¬ 𝐴 ∈ V → ( 𝑅 Po { 𝐴 } ↔ 𝑅 Po ∅ ) )
5 1 4 mpbiri ⊢ ( ¬ 𝐴 ∈ V → 𝑅 Po { 𝐴 } )
6 5 adantl ⊢ ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → 𝑅 Po { 𝐴 } )
7 brrelex1 ⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐴 ) → 𝐴 ∈ V )
8 7 stoic1a ⊢ ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → ¬ 𝐴 𝑅 𝐴 )
9 6 8 2thd ⊢ ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → ( 𝑅 Po { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )
10 9 ex ⊢ ( Rel 𝑅 → ( ¬ 𝐴 ∈ V → ( 𝑅 Po { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) ) )
11 df-po ⊢ ( 𝑅 Po { 𝐴 } ↔ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ∀ 𝑧 ∈ { 𝐴 } ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
12 breq2 ⊢ ( 𝑧 = 𝐴 → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑅 𝐴 ) )
13 12 anbi2d ⊢ ( 𝑧 = 𝐴 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐴 ) ) )
14 breq2 ⊢ ( 𝑧 = 𝐴 → ( 𝑥 𝑅 𝑧 ↔ 𝑥 𝑅 𝐴 ) )
15 13 14 imbi12d ⊢ ( 𝑧 = 𝐴 → ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐴 ) → 𝑥 𝑅 𝐴 ) ) )
16 15 anbi2d ⊢ ( 𝑧 = 𝐴 → ( ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐴 ) → 𝑥 𝑅 𝐴 ) ) ) )
17 16 ralsng ⊢ ( 𝐴 ∈ V → ( ∀ 𝑧 ∈ { 𝐴 } ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐴 ) → 𝑥 𝑅 𝐴 ) ) ) )
18 17 ralbidv ⊢ ( 𝐴 ∈ V → ( ∀ 𝑦 ∈ { 𝐴 } ∀ 𝑧 ∈ { 𝐴 } ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑦 ∈ { 𝐴 } ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐴 ) → 𝑥 𝑅 𝐴 ) ) ) )
19 simpl ⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐴 ) → 𝑥 𝑅 𝑦 )
20 breq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝐴 ) )
21 19 20 imbitrid ⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐴 ) → 𝑥 𝑅 𝐴 ) )
22 21 biantrud ⊢ ( 𝑦 = 𝐴 → ( ¬ 𝑥 𝑅 𝑥 ↔ ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐴 ) → 𝑥 𝑅 𝐴 ) ) ) )
23 22 bicomd ⊢ ( 𝑦 = 𝐴 → ( ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐴 ) → 𝑥 𝑅 𝐴 ) ) ↔ ¬ 𝑥 𝑅 𝑥 ) )
24 23 ralsng ⊢ ( 𝐴 ∈ V → ( ∀ 𝑦 ∈ { 𝐴 } ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐴 ) → 𝑥 𝑅 𝐴 ) ) ↔ ¬ 𝑥 𝑅 𝑥 ) )
25 18 24 bitrd ⊢ ( 𝐴 ∈ V → ( ∀ 𝑦 ∈ { 𝐴 } ∀ 𝑧 ∈ { 𝐴 } ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ¬ 𝑥 𝑅 𝑥 ) )
26 25 ralbidv ⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ∀ 𝑧 ∈ { 𝐴 } ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑥 ∈ { 𝐴 } ¬ 𝑥 𝑅 𝑥 ) )
27 breq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐴 ) → ( 𝑥 𝑅 𝑥 ↔ 𝐴 𝑅 𝐴 ) )
28 27 anidms ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝑅 𝑥 ↔ 𝐴 𝑅 𝐴 ) )
29 28 notbid ⊢ ( 𝑥 = 𝐴 → ( ¬ 𝑥 𝑅 𝑥 ↔ ¬ 𝐴 𝑅 𝐴 ) )
30 29 ralsng ⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ∈ { 𝐴 } ¬ 𝑥 𝑅 𝑥 ↔ ¬ 𝐴 𝑅 𝐴 ) )
31 26 30 bitrd ⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ∀ 𝑧 ∈ { 𝐴 } ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ¬ 𝐴 𝑅 𝐴 ) )
32 11 31 bitrid ⊢ ( 𝐴 ∈ V → ( 𝑅 Po { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )
33 10 32 pm2.61d2 ⊢ ( Rel 𝑅 → ( 𝑅 Po { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )