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

Metamath Proof Explorer

Theorem fr3nr

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

Ref Expression
Assertion fr3nr ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) )

Proof

Step Hyp Ref Expression
1 tpex ⊢ { 𝐵 , 𝐶 , 𝐷 } ∈ V
2 1 a1i ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → { 𝐵 , 𝐶 , 𝐷 } ∈ V )
3 simpl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝑅 Fr 𝐴 )
4 df-tp ⊢ { 𝐵 , 𝐶 , 𝐷 } = ( { 𝐵 , 𝐶 } ∪ { 𝐷 } )
5 simpr1 ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐵 ∈ 𝐴 )
6 simpr2 ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐶 ∈ 𝐴 )
7 5 6 prssd ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → { 𝐵 , 𝐶 } ⊆ 𝐴 )
8 simpr3 ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐷 ∈ 𝐴 )
9 8 snssd ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → { 𝐷 } ⊆ 𝐴 )
10 7 9 unssd ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ⊆ 𝐴 )
11 4 10 eqsstrid ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → { 𝐵 , 𝐶 , 𝐷 } ⊆ 𝐴 )
12 5 tpnzd ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → { 𝐵 , 𝐶 , 𝐷 } ≠ ∅ )
13 fri ⊢ ( ( ( { 𝐵 , 𝐶 , 𝐷 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( { 𝐵 , 𝐶 , 𝐷 } ⊆ 𝐴 ∧ { 𝐵 , 𝐶 , 𝐷 } ≠ ∅ ) ) → ∃ 𝑥 ∈ { 𝐵 , 𝐶 , 𝐷 } ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 )
14 2 3 11 12 13 syl22anc ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ∃ 𝑥 ∈ { 𝐵 , 𝐶 , 𝐷 } ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 )
15 breq2 ⊢ ( 𝑥 = 𝐵 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝐵 ) )
16 15 notbid ⊢ ( 𝑥 = 𝐵 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝐵 ) )
17 16 ralbidv ⊢ ( 𝑥 = 𝐵 → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 ) )
18 breq2 ⊢ ( 𝑥 = 𝐶 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝐶 ) )
19 18 notbid ⊢ ( 𝑥 = 𝐶 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝐶 ) )
20 19 ralbidv ⊢ ( 𝑥 = 𝐶 → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 ) )
21 breq2 ⊢ ( 𝑥 = 𝐷 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝐷 ) )
22 21 notbid ⊢ ( 𝑥 = 𝐷 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝐷 ) )
23 22 ralbidv ⊢ ( 𝑥 = 𝐷 → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 ) )
24 17 20 23 rextpg ⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ { 𝐵 , 𝐶 , 𝐷 } ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 ↔ ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 ) ) )
25 24 adantl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∃ 𝑥 ∈ { 𝐵 , 𝐶 , 𝐷 } ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 ↔ ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 ) ) )
26 14 25 mpbid ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 ) )
27 snsstp3 ⊢ { 𝐷 } ⊆ { 𝐵 , 𝐶 , 𝐷 }
28 snssg ⊢ ( 𝐷 ∈ 𝐴 → ( 𝐷 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ { 𝐷 } ⊆ { 𝐵 , 𝐶 , 𝐷 } ) )
29 8 28 syl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐷 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ { 𝐷 } ⊆ { 𝐵 , 𝐶 , 𝐷 } ) )
30 27 29 mpbiri ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐷 ∈ { 𝐵 , 𝐶 , 𝐷 } )
31 breq1 ⊢ ( 𝑦 = 𝐷 → ( 𝑦 𝑅 𝐵 ↔ 𝐷 𝑅 𝐵 ) )
32 31 notbid ⊢ ( 𝑦 = 𝐷 → ( ¬ 𝑦 𝑅 𝐵 ↔ ¬ 𝐷 𝑅 𝐵 ) )
33 32 rspcv ⊢ ( 𝐷 ∈ { 𝐵 , 𝐶 , 𝐷 } → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 → ¬ 𝐷 𝑅 𝐵 ) )
34 30 33 syl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 → ¬ 𝐷 𝑅 𝐵 ) )
35 snsstp1 ⊢ { 𝐵 } ⊆ { 𝐵 , 𝐶 , 𝐷 }
36 snssg ⊢ ( 𝐵 ∈ 𝐴 → ( 𝐵 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ { 𝐵 } ⊆ { 𝐵 , 𝐶 , 𝐷 } ) )
37 5 36 syl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐵 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ { 𝐵 } ⊆ { 𝐵 , 𝐶 , 𝐷 } ) )
38 35 37 mpbiri ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐵 ∈ { 𝐵 , 𝐶 , 𝐷 } )
39 breq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 𝑅 𝐶 ↔ 𝐵 𝑅 𝐶 ) )
40 39 notbid ⊢ ( 𝑦 = 𝐵 → ( ¬ 𝑦 𝑅 𝐶 ↔ ¬ 𝐵 𝑅 𝐶 ) )
41 40 rspcv ⊢ ( 𝐵 ∈ { 𝐵 , 𝐶 , 𝐷 } → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 → ¬ 𝐵 𝑅 𝐶 ) )
42 38 41 syl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 → ¬ 𝐵 𝑅 𝐶 ) )
43 snsstp2 ⊢ { 𝐶 } ⊆ { 𝐵 , 𝐶 , 𝐷 }
44 snssg ⊢ ( 𝐶 ∈ 𝐴 → ( 𝐶 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ { 𝐶 } ⊆ { 𝐵 , 𝐶 , 𝐷 } ) )
45 6 44 syl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐶 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ { 𝐶 } ⊆ { 𝐵 , 𝐶 , 𝐷 } ) )
46 43 45 mpbiri ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐶 ∈ { 𝐵 , 𝐶 , 𝐷 } )
47 breq1 ⊢ ( 𝑦 = 𝐶 → ( 𝑦 𝑅 𝐷 ↔ 𝐶 𝑅 𝐷 ) )
48 47 notbid ⊢ ( 𝑦 = 𝐶 → ( ¬ 𝑦 𝑅 𝐷 ↔ ¬ 𝐶 𝑅 𝐷 ) )
49 48 rspcv ⊢ ( 𝐶 ∈ { 𝐵 , 𝐶 , 𝐷 } → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 → ¬ 𝐶 𝑅 𝐷 ) )
50 46 49 syl ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 → ¬ 𝐶 𝑅 𝐷 ) )
51 34 42 50 3orim123d ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 ) → ( ¬ 𝐷 𝑅 𝐵 ∨ ¬ 𝐵 𝑅 𝐶 ∨ ¬ 𝐶 𝑅 𝐷 ) ) )
52 26 51 mpd ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ¬ 𝐷 𝑅 𝐵 ∨ ¬ 𝐵 𝑅 𝐶 ∨ ¬ 𝐶 𝑅 𝐷 ) )
53 3ianor ⊢ ( ¬ ( 𝐷 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ) ↔ ( ¬ 𝐷 𝑅 𝐵 ∨ ¬ 𝐵 𝑅 𝐶 ∨ ¬ 𝐶 𝑅 𝐷 ) )
54 52 53 sylibr ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ¬ ( 𝐷 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ) )
55 3anrot ⊢ ( ( 𝐷 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ) ↔ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) )
56 54 55 sylnib ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) )