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

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 biimtrid ⊢ ( 𝑅 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 biimtrid ⊢ ( 𝑅 Po 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ( I ↾ 𝐴 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
22 3 21 relssdv ⊢ ( 𝑅 Po 𝐴 → ( 𝑅 ∩ ( I ↾ 𝐴 ) ) ⊆ ∅ )
23 ss0 ⊢ ( ( 𝑅 ∩ ( I ↾ 𝐴 ) ) ⊆ ∅ → ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ )
24 22 23 syl ⊢ ( 𝑅 Po 𝐴 → ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ )