Theorem frirr

Description: A well-founded relation is irreflexive. Special case of Proposition 6.23 of TakeutiZaring p. 30. (Contributed by NM, 2-Jan-1994) (Revised by Mario Carneiro, 22-Jun-2015)

	Ref	Expression
Assertion	frirr	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 𝑅 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝑅 Fr 𝐴 )
2		snssi	⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 } ⊆ 𝐴 )
3	2	adantl	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝐵 } ⊆ 𝐴 )
4		snnzg	⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 } ≠ ∅ )
5	4	adantl	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝐵 } ≠ ∅ )
6		snex	⊢ { 𝐵 } ∈ V
7	6	frc	⊢ ( ( 𝑅 Fr 𝐴 ∧ { 𝐵 } ⊆ 𝐴 ∧ { 𝐵 } ≠ ∅ ) → ∃ 𝑦 ∈ { 𝐵 } { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ )
8	1 3 5 7	syl3anc	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ∃ 𝑦 ∈ { 𝐵 } { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ )
9		rabeq0	⊢ ( { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ∀ 𝑥 ∈ { 𝐵 } ¬ 𝑥 𝑅 𝑦 )
10		breq2	⊢ ( 𝑦 = 𝐵 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝐵 ) )
11	10	notbid	⊢ ( 𝑦 = 𝐵 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑥 𝑅 𝐵 ) )
12	11	ralbidv	⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑥 ∈ { 𝐵 } ¬ 𝑥 𝑅 𝑦 ↔ ∀ 𝑥 ∈ { 𝐵 } ¬ 𝑥 𝑅 𝐵 ) )
13	9 12	syl5bb	⊢ ( 𝑦 = 𝐵 → ( { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ∀ 𝑥 ∈ { 𝐵 } ¬ 𝑥 𝑅 𝐵 ) )
14	13	rexsng	⊢ ( 𝐵 ∈ 𝐴 → ( ∃ 𝑦 ∈ { 𝐵 } { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ∀ 𝑥 ∈ { 𝐵 } ¬ 𝑥 𝑅 𝐵 ) )
15		breq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 𝑅 𝐵 ↔ 𝐵 𝑅 𝐵 ) )
16	15	notbid	⊢ ( 𝑥 = 𝐵 → ( ¬ 𝑥 𝑅 𝐵 ↔ ¬ 𝐵 𝑅 𝐵 ) )
17	16	ralsng	⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑥 ∈ { 𝐵 } ¬ 𝑥 𝑅 𝐵 ↔ ¬ 𝐵 𝑅 𝐵 ) )
18	14 17	bitrd	⊢ ( 𝐵 ∈ 𝐴 → ( ∃ 𝑦 ∈ { 𝐵 } { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ¬ 𝐵 𝑅 𝐵 ) )
19	18	adantl	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ { 𝐵 } { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ¬ 𝐵 𝑅 𝐵 ) )
20	8 19	mpbid	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 𝑅 𝐵 )