Metamath Proof Explorer

Theorem fr2nr

Description: A well-founded relation has no 2-cycle loops. Special case of Proposition 6.23 of TakeutiZaring p. 30. (Contributed by NM, 30-May-1994) (Revised by Mario Carneiro, 22-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 prex ⊢ B C ∈ V
2 1 a1i ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → B C ∈ V
3 simpl ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → R Fr A
4 prssi ⊢ B ∈ A ∧ C ∈ A → B C ⊆ A
5 4 adantl ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → B C ⊆ A
6 prnzg ⊢ B ∈ A → B C ≠ ∅
7 6 ad2antrl ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → B C ≠ ∅
8 fri ⊢ B C ∈ V ∧ R Fr A ∧ B C ⊆ A ∧ B C ≠ ∅ → ∃ y ∈ B C ∀ x ∈ B C ¬ x R y
9 2 3 5 7 8 syl22anc ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → ∃ y ∈ B C ∀ x ∈ B C ¬ 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 C ¬ x R y ↔ ∀ x ∈ B C ¬ x R B
13 breq2 ⊢ y = C → x R y ↔ x R C
14 13 notbid ⊢ y = C → ¬ x R y ↔ ¬ x R C
15 14 ralbidv ⊢ y = C → ∀ x ∈ B C ¬ x R y ↔ ∀ x ∈ B C ¬ x R C
16 12 15 rexprg ⊢ B ∈ A ∧ C ∈ A → ∃ y ∈ B C ∀ x ∈ B C ¬ x R y ↔ ∀ x ∈ B C ¬ x R B ∨ ∀ x ∈ B C ¬ x R C
17 16 adantl ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → ∃ y ∈ B C ∀ x ∈ B C ¬ x R y ↔ ∀ x ∈ B C ¬ x R B ∨ ∀ x ∈ B C ¬ x R C
18 9 17 mpbid ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → ∀ x ∈ B C ¬ x R B ∨ ∀ x ∈ B C ¬ x R C
19 prid2g ⊢ C ∈ A → C ∈ B C
20 19 ad2antll ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → C ∈ B C
21 breq1 ⊢ x = C → x R B ↔ C R B
22 21 notbid ⊢ x = C → ¬ x R B ↔ ¬ C R B
23 22 rspcv ⊢ C ∈ B C → ∀ x ∈ B C ¬ x R B → ¬ C R B
24 20 23 syl ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → ∀ x ∈ B C ¬ x R B → ¬ C R B
25 prid1g ⊢ B ∈ A → B ∈ B C
26 25 ad2antrl ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → B ∈ B C
27 breq1 ⊢ x = B → x R C ↔ B R C
28 27 notbid ⊢ x = B → ¬ x R C ↔ ¬ B R C
29 28 rspcv ⊢ B ∈ B C → ∀ x ∈ B C ¬ x R C → ¬ B R C
30 26 29 syl ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → ∀ x ∈ B C ¬ x R C → ¬ B R C
31 24 30 orim12d ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → ∀ x ∈ B C ¬ x R B ∨ ∀ x ∈ B C ¬ x R C → ¬ C R B ∨ ¬ B R C
32 18 31 mpd ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → ¬ C R B ∨ ¬ B R C
33 32 orcomd ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → ¬ B R C ∨ ¬ C R B
34 ianor ⊢ ¬ B R C ∧ C R B ↔ ¬ B R C ∨ ¬ C R B
35 33 34 sylibr ⊢ R Fr A ∧ B ∈ A ∧ C ∈ A → ¬ B R C ∧ C R B