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 ⁡ R → R Po A ↔ ¬ A R A

Proof

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