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 { 𝐴 } ↔ ¬ 𝐴 𝑅 𝐴 ) )