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 breq1 ⊢ x = z → x R y ↔ z R y
10 9 rabeq0w ⊢ x ∈ B | x R y = ∅ ↔ ∀ z ∈ B ¬ z R y
11 breq2 ⊢ y = B → z R y ↔ z R B
12 11 notbid ⊢ y = B → ¬ z R y ↔ ¬ z R B
13 12 ralbidv ⊢ y = B → ∀ z ∈ B ¬ z R y ↔ ∀ z ∈ B ¬ z R B
14 10 13 syl5bb ⊢ y = B → x ∈ B | x R y = ∅ ↔ ∀ z ∈ B ¬ z R B
15 14 rexsng ⊢ B ∈ A → ∃ y ∈ B x ∈ B | x R y = ∅ ↔ ∀ z ∈ B ¬ z R B
16 breq1 ⊢ z = B → z R B ↔ B R B
17 16 notbid ⊢ z = B → ¬ z R B ↔ ¬ B R B
18 17 ralsng ⊢ B ∈ A → ∀ z ∈ B ¬ z R B ↔ ¬ B R B
19 15 18 bitrd ⊢ B ∈ A → ∃ y ∈ B x ∈ B | x R y = ∅ ↔ ¬ B R B
20 19 adantl ⊢ R Fr A ∧ B ∈ A → ∃ y ∈ B x ∈ B | x R y = ∅ ↔ ¬ B R B
21 8 20 mpbid ⊢ R Fr A ∧ B ∈ A → ¬ B R B