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 ⊢RFrA∧B∈A∧C∈A→¬BRC∧CRB

Proof

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