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⁡B→A∈⋃B↔suc⁡A∈B

Proof

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