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