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 → ( ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ∧ ( 𝐴 ∈ ∪ ∪ 𝑅 → 𝐴 𝑅 𝐴 ) ∧ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) → 𝐴 = 𝐵 ) ) )