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

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 ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐵 ) )

Proof

Step Hyp Ref Expression
1 prex ⊢ { 𝐵 , 𝐶 } ∈ V
2 1 a1i ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → { 𝐵 , 𝐶 } ∈ V )
3 simpl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → 𝑅 Fr 𝐴 )
4 prssi ⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → { 𝐵 , 𝐶 } ⊆ 𝐴 )
5 4 adantl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → { 𝐵 , 𝐶 } ⊆ 𝐴 )
6 prnzg ⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 , 𝐶 } ≠ ∅ )
7 6 ad2antrl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → { 𝐵 , 𝐶 } ≠ ∅ )
8 fri ⊢ ( ( ( { 𝐵 , 𝐶 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( { 𝐵 , 𝐶 } ⊆ 𝐴 ∧ { 𝐵 , 𝐶 } ≠ ∅ ) ) → ∃ 𝑦 ∈ { 𝐵 , 𝐶 } ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝑦 )
9 2 3 5 7 8 syl22anc ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ∃ 𝑦 ∈ { 𝐵 , 𝐶 } ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝑦 )
10 breq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝐵 ) )
11 10 notbid ⊢ ( 𝑦 = 𝐵 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑥 𝑅 𝐵 ) )
12 11 ralbidv ⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝑦 ↔ ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐵 ) )
13 breq2 ⊢ ( 𝑦 = 𝐶 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝐶 ) )
14 13 notbid ⊢ ( 𝑦 = 𝐶 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑥 𝑅 𝐶 ) )
15 14 ralbidv ⊢ ( 𝑦 = 𝐶 → ( ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝑦 ↔ ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐶 ) )
16 12 15 rexprg ⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ { 𝐵 , 𝐶 } ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝑦 ↔ ( ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐵 ∨ ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐶 ) ) )
17 16 adantl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ∃ 𝑦 ∈ { 𝐵 , 𝐶 } ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝑦 ↔ ( ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐵 ∨ ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐶 ) ) )
18 9 17 mpbid ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐵 ∨ ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐶 ) )
19 prid2g ⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ { 𝐵 , 𝐶 } )
20 19 ad2antll ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → 𝐶 ∈ { 𝐵 , 𝐶 } )
21 breq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 𝑅 𝐵 ↔ 𝐶 𝑅 𝐵 ) )
22 21 notbid ⊢ ( 𝑥 = 𝐶 → ( ¬ 𝑥 𝑅 𝐵 ↔ ¬ 𝐶 𝑅 𝐵 ) )
23 22 rspcv ⊢ ( 𝐶 ∈ { 𝐵 , 𝐶 } → ( ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐵 → ¬ 𝐶 𝑅 𝐵 ) )
24 20 23 syl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐵 → ¬ 𝐶 𝑅 𝐵 ) )
25 prid1g ⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ∈ { 𝐵 , 𝐶 } )
26 25 ad2antrl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → 𝐵 ∈ { 𝐵 , 𝐶 } )
27 breq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 𝑅 𝐶 ↔ 𝐵 𝑅 𝐶 ) )
28 27 notbid ⊢ ( 𝑥 = 𝐵 → ( ¬ 𝑥 𝑅 𝐶 ↔ ¬ 𝐵 𝑅 𝐶 ) )
29 28 rspcv ⊢ ( 𝐵 ∈ { 𝐵 , 𝐶 } → ( ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐶 → ¬ 𝐵 𝑅 𝐶 ) )
30 26 29 syl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐶 → ¬ 𝐵 𝑅 𝐶 ) )
31 24 30 orim12d ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ( ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐵 ∨ ∀ 𝑥 ∈ { 𝐵 , 𝐶 } ¬ 𝑥 𝑅 𝐶 ) → ( ¬ 𝐶 𝑅 𝐵 ∨ ¬ 𝐵 𝑅 𝐶 ) ) )
32 18 31 mpd ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ¬ 𝐶 𝑅 𝐵 ∨ ¬ 𝐵 𝑅 𝐶 ) )
33 32 orcomd ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ¬ 𝐵 𝑅 𝐶 ∨ ¬ 𝐶 𝑅 𝐵 ) )
34 ianor ⊢ ( ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐵 ) ↔ ( ¬ 𝐵 𝑅 𝐶 ∨ ¬ 𝐶 𝑅 𝐵 ) )
35 33 34 sylibr ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐵 ) )