Metamath Proof Explorer

Theorem frirr

Description: A well-founded relation is irreflexive. Special case of Proposition 6.23 of TakeutiZaring p. 30. (Contributed by NM, 2-Jan-1994) (Revised by Mario Carneiro, 22-Jun-2015)

Ref Expression
Assertion frirr ⊢ R Fr A ∧ B ∈ A → ¬ B R B

Proof

Step Hyp Ref Expression
1 simpl ⊢ R Fr A ∧ B ∈ A → R Fr A
2 snssi ⊢ B ∈ A → B ⊆ A
3 2 adantl ⊢ R Fr A ∧ B ∈ A → B ⊆ A
4 snnzg ⊢ B ∈ A → B ≠ ∅
5 4 adantl ⊢ R Fr A ∧ B ∈ A → B ≠ ∅
6 snex ⊢ B ∈ V
7 6 frc ⊢ R Fr A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ y ∈ B x ∈ B | x R y = ∅
8 1 3 5 7 syl3anc ⊢ R Fr A ∧ B ∈ A → ∃ y ∈ B x ∈ B | x R y = ∅
9 rabeq0 ⊢ x ∈ B | x R y = ∅ ↔ ∀ x ∈ B ¬ x R y
10 breq2 ⊢ y = B → x R y ↔ x R B
11 10 notbid ⊢ y = B → ¬ x R y ↔ ¬ x R B
12 11 ralbidv ⊢ y = B → ∀ x ∈ B ¬ x R y ↔ ∀ x ∈ B ¬ x R B
13 9 12 syl5bb ⊢ y = B → x ∈ B | x R y = ∅ ↔ ∀ x ∈ B ¬ x R B
14 13 rexsng ⊢ B ∈ A → ∃ y ∈ B x ∈ B | x R y = ∅ ↔ ∀ x ∈ B ¬ x R B
15 breq1 ⊢ x = B → x R B ↔ B R B
16 15 notbid ⊢ x = B → ¬ x R B ↔ ¬ B R B
17 16 ralsng ⊢ B ∈ A → ∀ x ∈ B ¬ x R B ↔ ¬ B R B
18 14 17 bitrd ⊢ B ∈ A → ∃ y ∈ B x ∈ B | x R y = ∅ ↔ ¬ B R B
19 18 adantl ⊢ R Fr A ∧ B ∈ A → ∃ y ∈ B x ∈ B | x R y = ∅ ↔ ¬ B R B
20 8 19 mpbid ⊢ R Fr A ∧ B ∈ A → ¬ B R B