Metamath Proof Explorer


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 ↾ 𝐴 ) ) = ∅ )