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

Metamath Proof Explorer

Theorem frss

Description: Subset theorem for the well-founded predicate. Exercise 1 of TakeutiZaring p. 31. (Contributed by NM, 3-Apr-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion frss ( 𝐴 ⊆ 𝐵 → ( 𝑅 Fr 𝐵 → 𝑅 Fr 𝐴 ) )

Proof

Step Hyp Ref Expression
1 sstr2 ⊢ ( 𝑥 ⊆ 𝐴 → ( 𝐴 ⊆ 𝐵 → 𝑥 ⊆ 𝐵 ) )
2 1 com12 ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) )
3 2 anim1d ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ≠ ∅ ) ) )
4 3 imim1d ⊢ ( 𝐴 ⊆ 𝐵 → ( ( ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) ) )
5 4 alimdv ⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ( ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) → ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) ) )
6 df-fr ⊢ ( 𝑅 Fr 𝐵 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
7 df-fr ⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
8 5 6 7 3imtr4g ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑅 Fr 𝐵 → 𝑅 Fr 𝐴 ) )