| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | uniexr 7784 | . . . 4
⊢ (∪ 𝐴
∈ dom card → 𝐴
∈ V) | 
| 2 |  | dfac8b 10072 | . . . 4
⊢ (∪ 𝐴
∈ dom card → ∃𝑟 𝑟 We ∪ 𝐴) | 
| 3 |  | dfac8c 10074 | . . . 4
⊢ (𝐴 ∈ V → (∃𝑟 𝑟 We ∪ 𝐴 → ∃𝑔∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))) | 
| 4 | 1, 2, 3 | sylc 65 | . . 3
⊢ (∪ 𝐴
∈ dom card → ∃𝑔∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) | 
| 5 | 4 | adantr 480 | . 2
⊢ ((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) | 
| 6 | 1 | ad2antrr 726 | . . . 4
⊢ (((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → 𝐴 ∈ V) | 
| 7 | 6 | mptexd 7245 | . . 3
⊢ (((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → (𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦)) ∈ V) | 
| 8 |  | nelne2 3039 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ ∅ ∈ 𝐴) → 𝑥 ≠ ∅) | 
| 9 | 8 | ancoms 458 | . . . . . . . . . . 11
⊢ ((¬
∅ ∈ 𝐴 ∧
𝑥 ∈ 𝐴) → 𝑥 ≠ ∅) | 
| 10 | 9 | adantll 714 | . . . . . . . . . 10
⊢ (((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ ∅) | 
| 11 |  | pm2.27 42 | . . . . . . . . . 10
⊢ (𝑥 ≠ ∅ → ((𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) → (𝑔‘𝑥) ∈ 𝑥)) | 
| 12 | 10, 11 | syl 17 | . . . . . . . . 9
⊢ (((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) → (𝑔‘𝑥) ∈ 𝑥)) | 
| 13 | 12 | ralimdva 3166 | . . . . . . . 8
⊢ ((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) → (∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝑥)) | 
| 14 | 13 | imp 406 | . . . . . . 7
⊢ (((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝑥) | 
| 15 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑔‘𝑥) = (𝑔‘𝑦)) | 
| 16 |  | id 22 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) | 
| 17 | 15, 16 | eleq12d 2834 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑔‘𝑥) ∈ 𝑥 ↔ (𝑔‘𝑦) ∈ 𝑦)) | 
| 18 | 17 | rspccva 3620 | . . . . . . 7
⊢
((∀𝑥 ∈
𝐴 (𝑔‘𝑥) ∈ 𝑥 ∧ 𝑦 ∈ 𝐴) → (𝑔‘𝑦) ∈ 𝑦) | 
| 19 | 14, 18 | sylan 580 | . . . . . 6
⊢ ((((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) ∧ 𝑦 ∈ 𝐴) → (𝑔‘𝑦) ∈ 𝑦) | 
| 20 |  | elunii 4911 | . . . . . 6
⊢ (((𝑔‘𝑦) ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑔‘𝑦) ∈ ∪ 𝐴) | 
| 21 | 19, 20 | sylancom 588 | . . . . 5
⊢ ((((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) ∧ 𝑦 ∈ 𝐴) → (𝑔‘𝑦) ∈ ∪ 𝐴) | 
| 22 | 21 | fmpttd 7134 | . . . 4
⊢ (((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → (𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦)):𝐴⟶∪ 𝐴) | 
| 23 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑔‘𝑦) = (𝑔‘𝑥)) | 
| 24 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦)) = (𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦)) | 
| 25 |  | fvex 6918 | . . . . . . . 8
⊢ (𝑔‘𝑥) ∈ V | 
| 26 | 23, 24, 25 | fvmpt 7015 | . . . . . . 7
⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦))‘𝑥) = (𝑔‘𝑥)) | 
| 27 | 26 | eleq1d 2825 | . . . . . 6
⊢ (𝑥 ∈ 𝐴 → (((𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦))‘𝑥) ∈ 𝑥 ↔ (𝑔‘𝑥) ∈ 𝑥)) | 
| 28 | 27 | ralbiia 3090 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 ((𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦))‘𝑥) ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝑥) | 
| 29 | 14, 28 | sylibr 234 | . . . 4
⊢ (((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → ∀𝑥 ∈ 𝐴 ((𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦))‘𝑥) ∈ 𝑥) | 
| 30 | 22, 29 | jca 511 | . . 3
⊢ (((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → ((𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦)):𝐴⟶∪ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ((𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦))‘𝑥) ∈ 𝑥)) | 
| 31 |  | feq1 6715 | . . . 4
⊢ (𝑓 = (𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦)) → (𝑓:𝐴⟶∪ 𝐴 ↔ (𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦)):𝐴⟶∪ 𝐴)) | 
| 32 |  | fveq1 6904 | . . . . . 6
⊢ (𝑓 = (𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦)) → (𝑓‘𝑥) = ((𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦))‘𝑥)) | 
| 33 | 32 | eleq1d 2825 | . . . . 5
⊢ (𝑓 = (𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦)) → ((𝑓‘𝑥) ∈ 𝑥 ↔ ((𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦))‘𝑥) ∈ 𝑥)) | 
| 34 | 33 | ralbidv 3177 | . . . 4
⊢ (𝑓 = (𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦)) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ((𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦))‘𝑥) ∈ 𝑥)) | 
| 35 | 31, 34 | anbi12d 632 | . . 3
⊢ (𝑓 = (𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦)) → ((𝑓:𝐴⟶∪ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥) ↔ ((𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦)):𝐴⟶∪ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ((𝑦 ∈ 𝐴 ↦ (𝑔‘𝑦))‘𝑥) ∈ 𝑥))) | 
| 36 | 7, 30, 35 | spcedv 3597 | . 2
⊢ (((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → ∃𝑓(𝑓:𝐴⟶∪ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥)) | 
| 37 | 5, 36 | exlimddv 1934 | 1
⊢ ((∪ 𝐴
∈ dom card ∧ ¬ ∅ ∈ 𝐴) → ∃𝑓(𝑓:𝐴⟶∪ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥)) |