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

Metamath Proof Explorer

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