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		breq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝑅 𝑦 ↔ 𝑧 𝑅 𝑦 ) )
10	9	rabeq0w	⊢ ( { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ∀ 𝑧 ∈ { 𝐵 } ¬ 𝑧 𝑅 𝑦 )
11		breq2	⊢ ( 𝑦 = 𝐵 → ( 𝑧 𝑅 𝑦 ↔ 𝑧 𝑅 𝐵 ) )
12	11	notbid	⊢ ( 𝑦 = 𝐵 → ( ¬ 𝑧 𝑅 𝑦 ↔ ¬ 𝑧 𝑅 𝐵 ) )
13	12	ralbidv	⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑧 ∈ { 𝐵 } ¬ 𝑧 𝑅 𝑦 ↔ ∀ 𝑧 ∈ { 𝐵 } ¬ 𝑧 𝑅 𝐵 ) )
14	10 13	bitrid	⊢ ( 𝑦 = 𝐵 → ( { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ∀ 𝑧 ∈ { 𝐵 } ¬ 𝑧 𝑅 𝐵 ) )
15	14	rexsng	⊢ ( 𝐵 ∈ 𝐴 → ( ∃ 𝑦 ∈ { 𝐵 } { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ∀ 𝑧 ∈ { 𝐵 } ¬ 𝑧 𝑅 𝐵 ) )
16		breq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 𝑅 𝐵 ↔ 𝐵 𝑅 𝐵 ) )
17	16	notbid	⊢ ( 𝑧 = 𝐵 → ( ¬ 𝑧 𝑅 𝐵 ↔ ¬ 𝐵 𝑅 𝐵 ) )
18	17	ralsng	⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑧 ∈ { 𝐵 } ¬ 𝑧 𝑅 𝐵 ↔ ¬ 𝐵 𝑅 𝐵 ) )
19	15 18	bitrd	⊢ ( 𝐵 ∈ 𝐴 → ( ∃ 𝑦 ∈ { 𝐵 } { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ¬ 𝐵 𝑅 𝐵 ) )
20	19	adantl	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ { 𝐵 } { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ¬ 𝐵 𝑅 𝐵 ) )
21	8 20	mpbid	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 𝑅 𝐵 )