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

Metamath Proof Explorer

Theorem oawordex

Description: Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of TakeutiZaring p. 59 and its converse. See oawordeu for uniqueness. (Contributed by NM, 12-Dec-2004)

		Ref	Expression
	Assertion	oawordex	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ On ( 𝐴 +_o 𝑥 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		oawordeu	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ∃! 𝑥 ∈ On ( 𝐴 +_o 𝑥 ) = 𝐵 )
2	1	ex	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ∃! 𝑥 ∈ On ( 𝐴 +_o 𝑥 ) = 𝐵 ) )
3		reurex	⊢ ( ∃! 𝑥 ∈ On ( 𝐴 +_o 𝑥 ) = 𝐵 → ∃ 𝑥 ∈ On ( 𝐴 +_o 𝑥 ) = 𝐵 )
4	2 3	syl6	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ∃ 𝑥 ∈ On ( 𝐴 +_o 𝑥 ) = 𝐵 ) )
5		oawordexr	⊢ ( ( 𝐴 ∈ On ∧ ∃ 𝑥 ∈ On ( 𝐴 +_o 𝑥 ) = 𝐵 ) → 𝐴 ⊆ 𝐵 )
6	5	ex	⊢ ( 𝐴 ∈ On → ( ∃ 𝑥 ∈ On ( 𝐴 +_o 𝑥 ) = 𝐵 → 𝐴 ⊆ 𝐵 ) )
7	6	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∃ 𝑥 ∈ On ( 𝐴 +_o 𝑥 ) = 𝐵 → 𝐴 ⊆ 𝐵 ) )
8	4 7	impbid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ On ( 𝐴 +_o 𝑥 ) = 𝐵 ) )