Proof of Theorem fnct
Step | Hyp | Ref
| Expression |
1 | | ctex 7970 |
. . . . 5
⊢ (𝐴 ≼ ω → 𝐴 ∈ V) |
2 | 1 | adantl 482 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → 𝐴 ∈ V) |
3 | | fndm 5990 |
. . . . . . . 8
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
4 | 3 | eleq1d 2686 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → (dom 𝐹 ∈ V ↔ 𝐴 ∈ V)) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → (dom 𝐹 ∈ V ↔ 𝐴 ∈ V)) |
6 | 2, 5 | mpbird 247 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → dom 𝐹 ∈ V) |
7 | | fnfun 5988 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
8 | 7 | adantr 481 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → Fun 𝐹) |
9 | | funrnex 7133 |
. . . . 5
⊢ (dom
𝐹 ∈ V → (Fun
𝐹 → ran 𝐹 ∈ V)) |
10 | 6, 8, 9 | sylc 65 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → ran 𝐹 ∈ V) |
11 | | xpexg 6960 |
. . . 4
⊢ ((𝐴 ∈ V ∧ ran 𝐹 ∈ V) → (𝐴 × ran 𝐹) ∈ V) |
12 | 2, 10, 11 | syl2anc 693 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → (𝐴 × ran 𝐹) ∈ V) |
13 | | simpl 473 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → 𝐹 Fn 𝐴) |
14 | | dffn3 6054 |
. . . . 5
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) |
15 | 13, 14 | sylib 208 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → 𝐹:𝐴⟶ran 𝐹) |
16 | | fssxp 6060 |
. . . 4
⊢ (𝐹:𝐴⟶ran 𝐹 → 𝐹 ⊆ (𝐴 × ran 𝐹)) |
17 | 15, 16 | syl 17 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → 𝐹 ⊆ (𝐴 × ran 𝐹)) |
18 | | ssdomg 8001 |
. . 3
⊢ ((𝐴 × ran 𝐹) ∈ V → (𝐹 ⊆ (𝐴 × ran 𝐹) → 𝐹 ≼ (𝐴 × ran 𝐹))) |
19 | 12, 17, 18 | sylc 65 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → 𝐹 ≼ (𝐴 × ran 𝐹)) |
20 | | xpdom1g 8057 |
. . . . 5
⊢ ((ran
𝐹 ∈ V ∧ 𝐴 ≼ ω) → (𝐴 × ran 𝐹) ≼ (ω × ran 𝐹)) |
21 | 10, 20 | sylancom 701 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → (𝐴 × ran 𝐹) ≼ (ω × ran 𝐹)) |
22 | | omex 8540 |
. . . . 5
⊢ ω
∈ V |
23 | | fnrndomg 9358 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝐹 Fn 𝐴 → ran 𝐹 ≼ 𝐴)) |
24 | 2, 13, 23 | sylc 65 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → ran 𝐹 ≼ 𝐴) |
25 | | domtr 8009 |
. . . . . 6
⊢ ((ran
𝐹 ≼ 𝐴 ∧ 𝐴 ≼ ω) → ran 𝐹 ≼
ω) |
26 | 24, 25 | sylancom 701 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → ran 𝐹 ≼
ω) |
27 | | xpdom2g 8056 |
. . . . 5
⊢ ((ω
∈ V ∧ ran 𝐹
≼ ω) → (ω × ran 𝐹) ≼ (ω ×
ω)) |
28 | 22, 26, 27 | sylancr 695 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → (ω ×
ran 𝐹) ≼ (ω
× ω)) |
29 | | domtr 8009 |
. . . 4
⊢ (((𝐴 × ran 𝐹) ≼ (ω × ran 𝐹) ∧ (ω × ran
𝐹) ≼ (ω ×
ω)) → (𝐴 ×
ran 𝐹) ≼ (ω
× ω)) |
30 | 21, 28, 29 | syl2anc 693 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → (𝐴 × ran 𝐹) ≼ (ω ×
ω)) |
31 | | xpomen 8838 |
. . 3
⊢ (ω
× ω) ≈ ω |
32 | | domentr 8015 |
. . 3
⊢ (((𝐴 × ran 𝐹) ≼ (ω × ω) ∧
(ω × ω) ≈ ω) → (𝐴 × ran 𝐹) ≼ ω) |
33 | 30, 31, 32 | sylancl 694 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → (𝐴 × ran 𝐹) ≼ ω) |
34 | | domtr 8009 |
. 2
⊢ ((𝐹 ≼ (𝐴 × ran 𝐹) ∧ (𝐴 × ran 𝐹) ≼ ω) → 𝐹 ≼ ω) |
35 | 19, 33, 34 | syl2anc 693 |
1
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → 𝐹 ≼ ω) |