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

Metamath Proof Explorer

Theorem pslem

Description: Lemma for psref and others. (Contributed by NM, 12-May-2008) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion pslem ( 𝑅 ∈ PosetRel → ( ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ∧ ( 𝐴 ∈ ∪ ∪ 𝑅 → 𝐴 𝑅 𝐴 ) ∧ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) → 𝐴 = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 psrel ⊢ ( 𝑅 ∈ PosetRel → Rel 𝑅 )
2 brrelex12 ⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
3 1 2 sylan ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
4 brrelex2 ⊢ ( ( Rel 𝑅 ∧ 𝐵 𝑅 𝐶 ) → 𝐶 ∈ V )
5 1 4 sylan ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐵 𝑅 𝐶 ) → 𝐶 ∈ V )
6 3 5 anim12dan ⊢ ( ( 𝑅 ∈ PosetRel ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐶 ∈ V ) )
7 pstr2 ⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )
8 cotr ⊢ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
9 7 8 sylib ⊢ ( 𝑅 ∈ PosetRel → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
10 9 adantr ⊢ ( ( 𝑅 ∈ PosetRel ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
11 simpr ⊢ ( ( 𝑅 ∈ PosetRel ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) → ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) )
12 breq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 𝑅 𝑦 ↔ 𝐴 𝑅 𝐵 ) )
13 12 3adant3 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ 𝐴 𝑅 𝐵 ) )
14 breq12 ⊢ ( ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝑦 𝑅 𝑧 ↔ 𝐵 𝑅 𝐶 ) )
15 14 3adant1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝑦 𝑅 𝑧 ↔ 𝐵 𝑅 𝐶 ) )
16 13 15 anbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ↔ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) )
17 breq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑧 = 𝐶 ) → ( 𝑥 𝑅 𝑧 ↔ 𝐴 𝑅 𝐶 ) )
18 17 3adant2 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝑥 𝑅 𝑧 ↔ 𝐴 𝑅 𝐶 ) )
19 16 18 imbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) )
20 19 spc3gv ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) )
21 20 3expa ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐶 ∈ V ) → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) )
22 6 10 11 21 syl3c ⊢ ( ( 𝑅 ∈ PosetRel ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) → 𝐴 𝑅 𝐶 )
23 22 ex ⊢ ( 𝑅 ∈ PosetRel → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )
24 psref2 ⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) )
25 asymref2 ⊢ ( ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ↔ ( ∀ 𝑥 ∈ ∪ ∪ 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ) )
26 25 simplbi ⊢ ( ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) → ∀ 𝑥 ∈ ∪ ∪ 𝑅 𝑥 𝑅 𝑥 )
27 breq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐴 ) → ( 𝑥 𝑅 𝑥 ↔ 𝐴 𝑅 𝐴 ) )
28 27 anidms ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝑅 𝑥 ↔ 𝐴 𝑅 𝐴 ) )
29 28 rspccv ⊢ ( ∀ 𝑥 ∈ ∪ ∪ 𝑅 𝑥 𝑅 𝑥 → ( 𝐴 ∈ ∪ ∪ 𝑅 → 𝐴 𝑅 𝐴 ) )
30 24 26 29 3syl ⊢ ( 𝑅 ∈ PosetRel → ( 𝐴 ∈ ∪ ∪ 𝑅 → 𝐴 𝑅 𝐴 ) )
31 3 adantrr ⊢ ( ( 𝑅 ∈ PosetRel ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
32 25 simprbi ⊢ ( ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
33 24 32 syl ⊢ ( 𝑅 ∈ PosetRel → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
34 33 adantr ⊢ ( ( 𝑅 ∈ PosetRel ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
35 simpr ⊢ ( ( 𝑅 ∈ PosetRel ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) ) → ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) )
36 breq12 ⊢ ( ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐴 ) → ( 𝑦 𝑅 𝑥 ↔ 𝐵 𝑅 𝐴 ) )
37 36 ancoms ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑦 𝑅 𝑥 ↔ 𝐵 𝑅 𝐴 ) )
38 12 37 anbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) ) )
39 eqeq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = 𝑦 ↔ 𝐴 = 𝐵 ) )
40 38 39 imbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) → 𝐴 = 𝐵 ) ) )
41 40 spc2gv ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) → 𝐴 = 𝐵 ) ) )
42 31 34 35 41 syl3c ⊢ ( ( 𝑅 ∈ PosetRel ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) ) → 𝐴 = 𝐵 )
43 42 ex ⊢ ( 𝑅 ∈ PosetRel → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) → 𝐴 = 𝐵 ) )
44 23 30 43 3jca ⊢ ( 𝑅 ∈ PosetRel → ( ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ∧ ( 𝐴 ∈ ∪ ∪ 𝑅 → 𝐴 𝑅 𝐴 ) ∧ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) → 𝐴 = 𝐵 ) ) )