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

Metamath Proof Explorer

Theorem ordsucuniel

Description: Given an element A of the union of an ordinal B , suc A is an element of B itself. (Contributed by Scott Fenton, 28-Mar-2012) (Proof shortened by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion ordsucuniel ( Ord 𝐵 → ( 𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 orduni ⊢ ( Ord 𝐵 → Ord ∪ 𝐵 )
2 ordelord ⊢ ( ( Ord ∪ 𝐵 ∧ 𝐴 ∈ ∪ 𝐵 ) → Ord 𝐴 )
3 2 ex ⊢ ( Ord ∪ 𝐵 → ( 𝐴 ∈ ∪ 𝐵 → Ord 𝐴 ) )
4 1 3 syl ⊢ ( Ord 𝐵 → ( 𝐴 ∈ ∪ 𝐵 → Ord 𝐴 ) )
5 ordelord ⊢ ( ( Ord 𝐵 ∧ suc 𝐴 ∈ 𝐵 ) → Ord suc 𝐴 )
6 ordsuc ⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 )
7 5 6 sylibr ⊢ ( ( Ord 𝐵 ∧ suc 𝐴 ∈ 𝐵 ) → Ord 𝐴 )
8 7 ex ⊢ ( Ord 𝐵 → ( suc 𝐴 ∈ 𝐵 → Ord 𝐴 ) )
9 ordsson ⊢ ( Ord 𝐵 → 𝐵 ⊆ On )
10 ordunisssuc ⊢ ( ( 𝐵 ⊆ On ∧ Ord 𝐴 ) → ( ∪ 𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ suc 𝐴 ) )
11 9 10 sylan ⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( ∪ 𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ suc 𝐴 ) )
12 ordtri1 ⊢ ( ( Ord ∪ 𝐵 ∧ Ord 𝐴 ) → ( ∪ 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ∪ 𝐵 ) )
13 1 12 sylan ⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( ∪ 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ∪ 𝐵 ) )
14 ordtri1 ⊢ ( ( Ord 𝐵 ∧ Ord suc 𝐴 ) → ( 𝐵 ⊆ suc 𝐴 ↔ ¬ suc 𝐴 ∈ 𝐵 ) )
15 6 14 sylan2b ⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐵 ⊆ suc 𝐴 ↔ ¬ suc 𝐴 ∈ 𝐵 ) )
16 11 13 15 3bitr3d ⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( ¬ 𝐴 ∈ ∪ 𝐵 ↔ ¬ suc 𝐴 ∈ 𝐵 ) )
17 16 con4bid ⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵 ) )
18 17 ex ⊢ ( Ord 𝐵 → ( Ord 𝐴 → ( 𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵 ) ) )
19 4 8 18 pm5.21ndd ⊢ ( Ord 𝐵 → ( 𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵 ) )