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

Metamath Proof Explorer

Theorem tz7.5

Description: A nonempty subclass of an ordinal class has a minimal element. Proposition 7.5 of TakeutiZaring p. 36. (Contributed by NM, 18-Feb-2004) (Revised by David Abernethy, 16-Mar-2011)

		Ref	Expression
	Assertion	tz7.5	⊢ ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ( 𝐵 ∩ 𝑥 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ordwe	⊢ ( Ord 𝐴 → E We 𝐴 )
2		wefrc	⊢ ( ( E We 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ( 𝐵 ∩ 𝑥 ) = ∅ )
3	1 2	syl3an1	⊢ ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ( 𝐵 ∩ 𝑥 ) = ∅ )