Metamath Proof Explorer

Theorem rankfu

Description: An upper bound on the rank of a function. (Contributed by GΓ©rard Lang, 5-Aug-2018)

Ref Expression
Hypotheses rankxpl.1 ⊒ 𝐴 ∈ V
rankxpl.2 ⊒ 𝐡 ∈ V
Assertion rankfu ( 𝐹 : 𝐴 ⟢ 𝐡 β†’ ( rank β€˜ 𝐹 ) βŠ† suc suc ( rank β€˜ ( 𝐴 βˆͺ 𝐡 ) ) )

Proof

Step Hyp Ref Expression
1 rankxpl.1 ⊒ 𝐴 ∈ V
2 rankxpl.2 ⊒ 𝐡 ∈ V
3 fssxp ⊒ ( 𝐹 : 𝐴 ⟢ 𝐡 β†’ 𝐹 βŠ† ( 𝐴 Γ— 𝐡 ) )
4 1 2 xpex ⊒ ( 𝐴 Γ— 𝐡 ) ∈ V
5 4 rankss ⊒ ( 𝐹 βŠ† ( 𝐴 Γ— 𝐡 ) β†’ ( rank β€˜ 𝐹 ) βŠ† ( rank β€˜ ( 𝐴 Γ— 𝐡 ) ) )
6 1 2 rankxpu ⊒ ( rank β€˜ ( 𝐴 Γ— 𝐡 ) ) βŠ† suc suc ( rank β€˜ ( 𝐴 βˆͺ 𝐡 ) )
7 5 6 sstrdi ⊒ ( 𝐹 βŠ† ( 𝐴 Γ— 𝐡 ) β†’ ( rank β€˜ 𝐹 ) βŠ† suc suc ( rank β€˜ ( 𝐴 βˆͺ 𝐡 ) ) )
8 3 7 syl ⊒ ( 𝐹 : 𝐴 ⟢ 𝐡 β†’ ( rank β€˜ 𝐹 ) βŠ† suc suc ( rank β€˜ ( 𝐴 βˆͺ 𝐡 ) ) )