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