Proof of Theorem marypha2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | marypha2.a | . . 3
⊢ (𝜑 → 𝐴 ∈ Fin) | 
| 2 |  | marypha2.b | . . . 4
⊢ (𝜑 → 𝐹:𝐴⟶Fin) | 
| 3 | 2, 1 | unirnffid 9388 | . . 3
⊢ (𝜑 → ∪ ran 𝐹 ∈ Fin) | 
| 4 |  | eqid 2736 | . . . . 5
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) = ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) | 
| 5 | 4 | marypha2lem1 9476 | . . . 4
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⊆ (𝐴 × ∪ ran
𝐹) | 
| 6 | 5 | a1i 11 | . . 3
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⊆ (𝐴 × ∪ ran
𝐹)) | 
| 7 |  | marypha2.c | . . . 4
⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → 𝑑 ≼ ∪ (𝐹 “ 𝑑)) | 
| 8 | 2 | ffnd 6736 | . . . . 5
⊢ (𝜑 → 𝐹 Fn 𝐴) | 
| 9 | 4 | marypha2lem4 9479 | . . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑑 ⊆ 𝐴) → (∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) “ 𝑑) = ∪ (𝐹 “ 𝑑)) | 
| 10 | 8, 9 | sylan 580 | . . . 4
⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → (∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) “ 𝑑) = ∪ (𝐹 “ 𝑑)) | 
| 11 | 7, 10 | breqtrrd 5170 | . . 3
⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → 𝑑 ≼ (∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) “ 𝑑)) | 
| 12 | 1, 3, 6, 11 | marypha1 9475 | . 2
⊢ (𝜑 → ∃𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))𝑔:𝐴–1-1→∪ ran 𝐹) | 
| 13 |  | df-rex 3070 | . . 3
⊢
(∃𝑔 ∈
𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))𝑔:𝐴–1-1→∪ ran 𝐹 ↔ ∃𝑔(𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) | 
| 14 |  | ssv 4007 | . . . . . . . 8
⊢ ∪ ran 𝐹 ⊆ V | 
| 15 |  | f1ss 6808 | . . . . . . . 8
⊢ ((𝑔:𝐴–1-1→∪ ran 𝐹 ∧ ∪ ran 𝐹 ⊆ V) → 𝑔:𝐴–1-1→V) | 
| 16 | 14, 15 | mpan2 691 | . . . . . . 7
⊢ (𝑔:𝐴–1-1→∪ ran 𝐹 → 𝑔:𝐴–1-1→V) | 
| 17 | 16 | ad2antll 729 | . . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → 𝑔:𝐴–1-1→V) | 
| 18 |  | elpwi 4606 | . . . . . . . 8
⊢ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) → 𝑔 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))) | 
| 19 | 18 | ad2antrl 728 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → 𝑔 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))) | 
| 20 |  | f1fn 6804 | . . . . . . . . 9
⊢ (𝑔:𝐴–1-1→∪ ran 𝐹 → 𝑔 Fn 𝐴) | 
| 21 | 20 | ad2antll 729 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → 𝑔 Fn 𝐴) | 
| 22 | 4 | marypha2lem3 9478 | . . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝑔 Fn 𝐴) → (𝑔 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) | 
| 23 | 8, 21, 22 | syl2an2r 685 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → (𝑔 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) | 
| 24 | 19, 23 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)) | 
| 25 | 17, 24 | jca 511 | . . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹)) → (𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) | 
| 26 | 25 | ex 412 | . . . 4
⊢ (𝜑 → ((𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹) → (𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)))) | 
| 27 | 26 | eximdv 1916 | . . 3
⊢ (𝜑 → (∃𝑔(𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ∧ 𝑔:𝐴–1-1→∪ ran 𝐹) → ∃𝑔(𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)))) | 
| 28 | 13, 27 | biimtrid 242 | . 2
⊢ (𝜑 → (∃𝑔 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))𝑔:𝐴–1-1→∪ ran 𝐹 → ∃𝑔(𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)))) | 
| 29 | 12, 28 | mpd 15 | 1
⊢ (𝜑 → ∃𝑔(𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) |