Proof of Theorem marypha2
Step | Hyp | Ref
| Expression |
1 | | marypha2.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
2 | | marypha2.b |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶Fin) |
3 | 2, 1 | unirnffid 9332 |
. . 3
⊢ (𝜑 → ∪ ran 𝐹 ∈ Fin) |
4 | | eqid 2733 |
. . . . 5
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) = ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) |
5 | 4 | marypha2lem1 9417 |
. . . 4
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⊆ (𝐴 × ∪ ran
𝐹) |
6 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⊆ (𝐴 × ∪ ran
𝐹)) |
7 | | marypha2.c |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → 𝑑 ≼ ∪ (𝐹 “ 𝑑)) |
8 | 2 | ffnd 6708 |
. . . . 5
⊢ (𝜑 → 𝐹 Fn 𝐴) |
9 | 4 | marypha2lem4 9420 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑑 ⊆ 𝐴) → (∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) “ 𝑑) = ∪ (𝐹 “ 𝑑)) |
10 | 8, 9 | sylan 581 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) “ 𝑑) = ∪ (𝐹 “ 𝑑)) |
11 | 7, 10 | breqtrrd 5172 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → 𝑑 ≼ (∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) “ 𝑑)) |
12 | 1, 3, 6, 11 | marypha1 9416 |
. 2
⊢ (𝜑 → ∃𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))𝑔:𝐴–1-1→∪ ran 𝐹) |
13 | | df-rex 3072 |
. . 3
⊢
(∃𝑔 ∈
𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))𝑔:𝐴–1-1→∪ ran 𝐹 ↔ ∃𝑔(𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) |
14 | | ssv 4004 |
. . . . . . . 8
⊢ ∪ ran 𝐹 ⊆ V |
15 | | f1ss 6783 |
. . . . . . . 8
⊢ ((𝑔:𝐴–1-1→∪ ran 𝐹 ∧ ∪ ran 𝐹 ⊆ V) → 𝑔:𝐴–1-1→V) |
16 | 14, 15 | mpan2 690 |
. . . . . . 7
⊢ (𝑔:𝐴–1-1→∪ ran 𝐹 → 𝑔:𝐴–1-1→V) |
17 | 16 | ad2antll 728 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → 𝑔:𝐴–1-1→V) |
18 | | elpwi 4605 |
. . . . . . . 8
⊢ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) → 𝑔 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))) |
19 | 18 | ad2antrl 727 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → 𝑔 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))) |
20 | | f1fn 6778 |
. . . . . . . . 9
⊢ (𝑔:𝐴–1-1→∪ ran 𝐹 → 𝑔 Fn 𝐴) |
21 | 20 | ad2antll 728 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → 𝑔 Fn 𝐴) |
22 | 4 | marypha2lem3 9419 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝑔 Fn 𝐴) → (𝑔 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) |
23 | 8, 21, 22 | syl2an2r 684 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → (𝑔 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) |
24 | 19, 23 | mpbid 231 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)) |
25 | 17, 24 | jca 513 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → (𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) |
26 | 25 | ex 414 |
. . . 4
⊢ (𝜑 → ((𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹) → (𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)))) |
27 | 26 | eximdv 1921 |
. . 3
⊢ (𝜑 → (∃𝑔(𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹) → ∃𝑔(𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)))) |
28 | 13, 27 | biimtrid 241 |
. 2
⊢ (𝜑 → (∃𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))𝑔:𝐴–1-1→∪ ran 𝐹 → ∃𝑔(𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)))) |
29 | 12, 28 | mpd 15 |
1
⊢ (𝜑 → ∃𝑔(𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) |