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 ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω ) → 𝐹 ≼ ω )

Proof

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