Metamath Proof Explorer

Theorem fnctOLD

Description: Obsolete version of fnct as of 26-Aug-2026. (Contributed by Thierry Arnoux, 29-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion fnctOLD ⊢ F Fn A ∧ A ≼ ω → F ≼ ω

Proof

Step Hyp Ref Expression
1 ctex ⊢ A ≼ ω → A ∈ V
2 1 adantl ⊢ F Fn A ∧ A ≼ ω → A ∈ V
3 fndm ⊢ F Fn A → dom ⁡ F = A
4 3 eleq1d ⊢ F Fn A → dom ⁡ F ∈ V ↔ A ∈ V
5 4 adantr ⊢ F Fn A ∧ A ≼ ω → dom ⁡ F ∈ V ↔ A ∈ V
6 2 5 mpbird ⊢ F Fn A ∧ A ≼ ω → dom ⁡ F ∈ V
7 fnfun ⊢ F Fn A → Fun ⁡ F
8 7 adantr ⊢ F Fn A ∧ A ≼ ω → Fun ⁡ F
9 funrnex ⊢ dom ⁡ F ∈ V → Fun ⁡ F → ran ⁡ F ∈ V
10 6 8 9 sylc ⊢ F Fn A ∧ A ≼ ω → ran ⁡ F ∈ V
11 2 10 xpexd ⊢ F Fn A ∧ A ≼ ω → A × ran ⁡ F ∈ V
12 dffn3 ⊢ F Fn A ↔ F : A ⟶ ran ⁡ F
13 12 birani ⊢ F Fn A ∧ A ≼ ω → F : A ⟶ ran ⁡ F
14 fssxp ⊢ F : A ⟶ ran ⁡ F → F ⊆ A × ran ⁡ F
15 13 14 syl ⊢ F Fn A ∧ A ≼ ω → F ⊆ A × ran ⁡ F
16 ssdomg ⊢ A × ran ⁡ F ∈ V → F ⊆ A × ran ⁡ F → F ≼ A × ran ⁡ F
17 11 15 16 sylc ⊢ F Fn A ∧ A ≼ ω → F ≼ A × ran ⁡ F
18 xpdom1g ⊢ ran ⁡ F ∈ V ∧ A ≼ ω → A × ran ⁡ F ≼ ω × ran ⁡ F
19 10 18 sylancom ⊢ F Fn A ∧ A ≼ ω → A × ran ⁡ F ≼ ω × ran ⁡ F
20 omex ⊢ ω ∈ V
21 simpl ⊢ F Fn A ∧ A ≼ ω → F Fn A
22 fnrndomg ⊢ A ∈ V → F Fn A → ran ⁡ F ≼ A
23 2 21 22 sylc ⊢ F Fn A ∧ A ≼ ω → ran ⁡ F ≼ A
24 domtr ⊢ ran ⁡ F ≼ A ∧ A ≼ ω → ran ⁡ F ≼ ω
25 23 24 sylancom ⊢ F Fn A ∧ A ≼ ω → ran ⁡ F ≼ ω
26 xpdom2g ⊢ ω ∈ V ∧ ran ⁡ F ≼ ω → ω × ran ⁡ F ≼ ω × ω
27 20 25 26 sylancr ⊢ F Fn A ∧ A ≼ ω → ω × ran ⁡ F ≼ ω × ω
28 domtr ⊢ A × ran ⁡ F ≼ ω × ran ⁡ F ∧ ω × ran ⁡ F ≼ ω × ω → A × ran ⁡ F ≼ ω × ω
29 19 27 28 syl2anc ⊢ F Fn A ∧ A ≼ ω → A × ran ⁡ F ≼ ω × ω
30 xpomen ⊢ ω × ω ≈ ω
31 domentr ⊢ A × ran ⁡ F ≼ ω × ω ∧ ω × ω ≈ ω → A × ran ⁡ F ≼ ω
32 29 30 31 sylancl ⊢ F Fn A ∧ A ≼ ω → A × ran ⁡ F ≼ ω
33 domtr ⊢ F ≼ A × ran ⁡ F ∧ A × ran ⁡ F ≼ ω → F ≼ ω
34 17 32 33 syl2anc ⊢ F Fn A ∧ A ≼ ω → F ≼ ω