Theorem poirr2

Description: A partial order is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015) (Proof shortened by Peter Mazsa, 2-Oct-2022)

	Ref	Expression
Assertion	poirr2	⊢ ( 𝑅 Po 𝐴 → ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		relres	⊢ Rel ( I ↾ 𝐴 )
2		relin2	⊢ ( Rel ( I ↾ 𝐴 ) → Rel ( 𝑅 ∩ ( I ↾ 𝐴 ) ) )
3	1 2	mp1i	⊢ ( 𝑅 Po 𝐴 → Rel ( 𝑅 ∩ ( I ↾ 𝐴 ) ) )
4		df-br	⊢ ( 𝑥 ( 𝑅 ∩ ( I ↾ 𝐴 ) ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ( I ↾ 𝐴 ) ) )
5		brin	⊢ ( 𝑥 ( 𝑅 ∩ ( I ↾ 𝐴 ) ) 𝑦 ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑥 ( I ↾ 𝐴 ) 𝑦 ) )
6	4 5	bitr3i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ( I ↾ 𝐴 ) ) ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑥 ( I ↾ 𝐴 ) 𝑦 ) )
7		vex	⊢ 𝑦 ∈ V
8	7	brresi	⊢ ( 𝑥 ( I ↾ 𝐴 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 I 𝑦 ) )
9		poirr	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 𝑅 𝑥 )
10	7	ideq	⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
11		breq2	⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) )
12	10 11	sylbi	⊢ ( 𝑥 I 𝑦 → ( 𝑥 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) )
13	12	notbid	⊢ ( 𝑥 I 𝑦 → ( ¬ 𝑥 𝑅 𝑥 ↔ ¬ 𝑥 𝑅 𝑦 ) )
14	9 13	syl5ibcom	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 I 𝑦 → ¬ 𝑥 𝑅 𝑦 ) )
15	14	expimpd	⊢ ( 𝑅 Po 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 I 𝑦 ) → ¬ 𝑥 𝑅 𝑦 ) )
16	8 15	syl5bi	⊢ ( 𝑅 Po 𝐴 → ( 𝑥 ( I ↾ 𝐴 ) 𝑦 → ¬ 𝑥 𝑅 𝑦 ) )
17	16	con2d	⊢ ( 𝑅 Po 𝐴 → ( 𝑥 𝑅 𝑦 → ¬ 𝑥 ( I ↾ 𝐴 ) 𝑦 ) )
18		imnan	⊢ ( ( 𝑥 𝑅 𝑦 → ¬ 𝑥 ( I ↾ 𝐴 ) 𝑦 ) ↔ ¬ ( 𝑥 𝑅 𝑦 ∧ 𝑥 ( I ↾ 𝐴 ) 𝑦 ) )
19	17 18	sylib	⊢ ( 𝑅 Po 𝐴 → ¬ ( 𝑥 𝑅 𝑦 ∧ 𝑥 ( I ↾ 𝐴 ) 𝑦 ) )
20	19	pm2.21d	⊢ ( 𝑅 Po 𝐴 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ( I ↾ 𝐴 ) 𝑦 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
21	6 20	syl5bi	⊢ ( 𝑅 Po 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ( I ↾ 𝐴 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
22	3 21	relssdv	⊢ ( 𝑅 Po 𝐴 → ( 𝑅 ∩ ( I ↾ 𝐴 ) ) ⊆ ∅ )
23		ss0	⊢ ( ( 𝑅 ∩ ( I ↾ 𝐴 ) ) ⊆ ∅ → ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ )
24	22 23	syl	⊢ ( 𝑅 Po 𝐴 → ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ )