Proof of Theorem marypha2
Step | Hyp | Ref
| Expression |
1 | | marypha2.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
2 | | marypha2.b |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶Fin) |
3 | 2, 1 | unirnffid 8141 |
. . 3
⊢ (𝜑 → ∪ ran 𝐹 ∈ Fin) |
4 | | eqid 2610 |
. . . . 5
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) = ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) |
5 | 4 | marypha2lem1 8224 |
. . . 4
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⊆ (𝐴 × ∪ ran
𝐹) |
6 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⊆ (𝐴 × ∪ ran
𝐹)) |
7 | | marypha2.c |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → 𝑑 ≼ ∪ (𝐹 “ 𝑑)) |
8 | | ffn 5958 |
. . . . . 6
⊢ (𝐹:𝐴⟶Fin → 𝐹 Fn 𝐴) |
9 | 2, 8 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 Fn 𝐴) |
10 | 4 | marypha2lem4 8227 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑑 ⊆ 𝐴) → (∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) “ 𝑑) = ∪ (𝐹 “ 𝑑)) |
11 | 9, 10 | sylan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) “ 𝑑) = ∪ (𝐹 “ 𝑑)) |
12 | 7, 11 | breqtrrd 4611 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → 𝑑 ≼ (∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) “ 𝑑)) |
13 | 1, 3, 6, 12 | marypha1 8223 |
. 2
⊢ (𝜑 → ∃𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))𝑔:𝐴–1-1→∪ ran 𝐹) |
14 | | df-rex 2902 |
. . 3
⊢
(∃𝑔 ∈
𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))𝑔:𝐴–1-1→∪ ran 𝐹 ↔ ∃𝑔(𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) |
15 | | ssv 3588 |
. . . . . . . 8
⊢ ∪ ran 𝐹 ⊆ V |
16 | | f1ss 6019 |
. . . . . . . 8
⊢ ((𝑔:𝐴–1-1→∪ ran 𝐹 ∧ ∪ ran 𝐹 ⊆ V) → 𝑔:𝐴–1-1→V) |
17 | 15, 16 | mpan2 703 |
. . . . . . 7
⊢ (𝑔:𝐴–1-1→∪ ran 𝐹 → 𝑔:𝐴–1-1→V) |
18 | 17 | ad2antll 761 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → 𝑔:𝐴–1-1→V) |
19 | | elpwi 4117 |
. . . . . . . 8
⊢ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) → 𝑔 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))) |
20 | 19 | ad2antrl 760 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → 𝑔 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))) |
21 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → 𝐹 Fn 𝐴) |
22 | | f1fn 6015 |
. . . . . . . . 9
⊢ (𝑔:𝐴–1-1→∪ ran 𝐹 → 𝑔 Fn 𝐴) |
23 | 22 | ad2antll 761 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → 𝑔 Fn 𝐴) |
24 | 4 | marypha2lem3 8226 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝑔 Fn 𝐴) → (𝑔 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) |
25 | 21, 23, 24 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → (𝑔 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) |
26 | 20, 25 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)) |
27 | 18, 26 | jca 553 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → (𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) |
28 | 27 | ex 449 |
. . . 4
⊢ (𝜑 → ((𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹) → (𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)))) |
29 | 28 | eximdv 1833 |
. . 3
⊢ (𝜑 → (∃𝑔(𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹) → ∃𝑔(𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)))) |
30 | 14, 29 | syl5bi 231 |
. 2
⊢ (𝜑 → (∃𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))𝑔:𝐴–1-1→∪ ran 𝐹 → ∃𝑔(𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)))) |
31 | 13, 30 | mpd 15 |
1
⊢ (𝜑 → ∃𝑔(𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) |