Metamath Proof Explorer

Theorem hfunOLD

Description: Obsolete version of hfun as of 17-Sep-2026. (Contributed by Scott Fenton, 15-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion hfunOLD Could not format assertion : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. HF ) with typecode |-

Proof

Step Hyp Ref Expression
1 rankung Could not format ( ( A e. HF /\ B e. HF ) -> ( rank ` ( A u. B ) ) = ( ( rank ` A ) u. ( rank ` B ) ) ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( rank ` ( A u. B ) ) = ( ( rank ` A ) u. ( rank ` B ) ) ) with typecode |-
2 elhf2g Could not format ( A e. HF -> ( A e. HF <-> ( rank ` A ) e. _om ) ) : No typesetting found for |- ( A e. HF -> ( A e. HF <-> ( rank ` A ) e. _om ) ) with typecode |-
3 2 ibi Could not format ( A e. HF -> ( rank ` A ) e. _om ) : No typesetting found for |- ( A e. HF -> ( rank ` A ) e. _om ) with typecode |-
4 elhf2g Could not format ( B e. HF -> ( B e. HF <-> ( rank ` B ) e. _om ) ) : No typesetting found for |- ( B e. HF -> ( B e. HF <-> ( rank ` B ) e. _om ) ) with typecode |-
5 4 ibi Could not format ( B e. HF -> ( rank ` B ) e. _om ) : No typesetting found for |- ( B e. HF -> ( rank ` B ) e. _om ) with typecode |-
6 eleq1a ⊢ rank ⁡ B ∈ ω → rank ⁡ A ∪ rank ⁡ B = rank ⁡ B → rank ⁡ A ∪ rank ⁡ B ∈ ω
7 6 adantl ⊢ rank ⁡ A ∈ ω ∧ rank ⁡ B ∈ ω → rank ⁡ A ∪ rank ⁡ B = rank ⁡ B → rank ⁡ A ∪ rank ⁡ B ∈ ω
8 uncom ⊢ rank ⁡ B ∪ rank ⁡ A = rank ⁡ A ∪ rank ⁡ B
9 8 eqeq1i ⊢ rank ⁡ B ∪ rank ⁡ A = rank ⁡ A ↔ rank ⁡ A ∪ rank ⁡ B = rank ⁡ A
10 9 biimpi ⊢ rank ⁡ B ∪ rank ⁡ A = rank ⁡ A → rank ⁡ A ∪ rank ⁡ B = rank ⁡ A
11 10 eleq1d ⊢ rank ⁡ B ∪ rank ⁡ A = rank ⁡ A → rank ⁡ A ∪ rank ⁡ B ∈ ω ↔ rank ⁡ A ∈ ω
12 11 biimprcd ⊢ rank ⁡ A ∈ ω → rank ⁡ B ∪ rank ⁡ A = rank ⁡ A → rank ⁡ A ∪ rank ⁡ B ∈ ω
13 12 adantr ⊢ rank ⁡ A ∈ ω ∧ rank ⁡ B ∈ ω → rank ⁡ B ∪ rank ⁡ A = rank ⁡ A → rank ⁡ A ∪ rank ⁡ B ∈ ω
14 nnord ⊢ rank ⁡ A ∈ ω → Ord ⁡ rank ⁡ A
15 nnord ⊢ rank ⁡ B ∈ ω → Ord ⁡ rank ⁡ B
16 ordtri2or2 ⊢ Ord ⁡ rank ⁡ A ∧ Ord ⁡ rank ⁡ B → rank ⁡ A ⊆ rank ⁡ B ∨ rank ⁡ B ⊆ rank ⁡ A
17 14 15 16 syl2an ⊢ rank ⁡ A ∈ ω ∧ rank ⁡ B ∈ ω → rank ⁡ A ⊆ rank ⁡ B ∨ rank ⁡ B ⊆ rank ⁡ A
18 ssequn1 ⊢ rank ⁡ A ⊆ rank ⁡ B ↔ rank ⁡ A ∪ rank ⁡ B = rank ⁡ B
19 ssequn1 ⊢ rank ⁡ B ⊆ rank ⁡ A ↔ rank ⁡ B ∪ rank ⁡ A = rank ⁡ A
20 18 19 orbi12i ⊢ rank ⁡ A ⊆ rank ⁡ B ∨ rank ⁡ B ⊆ rank ⁡ A ↔ rank ⁡ A ∪ rank ⁡ B = rank ⁡ B ∨ rank ⁡ B ∪ rank ⁡ A = rank ⁡ A
21 17 20 sylib ⊢ rank ⁡ A ∈ ω ∧ rank ⁡ B ∈ ω → rank ⁡ A ∪ rank ⁡ B = rank ⁡ B ∨ rank ⁡ B ∪ rank ⁡ A = rank ⁡ A
22 7 13 21 mpjaod ⊢ rank ⁡ A ∈ ω ∧ rank ⁡ B ∈ ω → rank ⁡ A ∪ rank ⁡ B ∈ ω
23 3 5 22 syl2an Could not format ( ( A e. HF /\ B e. HF ) -> ( ( rank ` A ) u. ( rank ` B ) ) e. _om ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( ( rank ` A ) u. ( rank ` B ) ) e. _om ) with typecode |-
24 1 23 eqeltrd Could not format ( ( A e. HF /\ B e. HF ) -> ( rank ` ( A u. B ) ) e. _om ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( rank ` ( A u. B ) ) e. _om ) with typecode |-
25 unexg Could not format ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. _V ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. _V ) with typecode |-
26 elhf2g Could not format ( ( A u. B ) e. _V -> ( ( A u. B ) e. HF <-> ( rank ` ( A u. B ) ) e. _om ) ) : No typesetting found for |- ( ( A u. B ) e. _V -> ( ( A u. B ) e. HF <-> ( rank ` ( A u. B ) ) e. _om ) ) with typecode |-
27 25 26 syl Could not format ( ( A e. HF /\ B e. HF ) -> ( ( A u. B ) e. HF <-> ( rank ` ( A u. B ) ) e. _om ) ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( ( A u. B ) e. HF <-> ( rank ` ( A u. B ) ) e. _om ) ) with typecode |-
28 24 27 mpbird Could not format ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. HF ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. HF ) with typecode |-