| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | unirnmap.x | . . . . . . . 8
⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑m 𝐴)) | 
| 2 | 1 | sselda 3983 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔 ∈ (𝐵 ↑m 𝐴)) | 
| 3 |  | elmapfn 8905 | . . . . . . 7
⊢ (𝑔 ∈ (𝐵 ↑m 𝐴) → 𝑔 Fn 𝐴) | 
| 4 | 2, 3 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔 Fn 𝐴) | 
| 5 |  | simplr 769 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ 𝑋) | 
| 6 |  | dffn3 6748 | . . . . . . . . . . . 12
⊢ (𝑔 Fn 𝐴 ↔ 𝑔:𝐴⟶ran 𝑔) | 
| 7 | 4, 6 | sylib 218 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔:𝐴⟶ran 𝑔) | 
| 8 | 7 | ffvelcdmda 7104 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ran 𝑔) | 
| 9 |  | rneq 5947 | . . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → ran 𝑓 = ran 𝑔) | 
| 10 | 9 | eleq2d 2827 | . . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ((𝑔‘𝑥) ∈ ran 𝑓 ↔ (𝑔‘𝑥) ∈ ran 𝑔)) | 
| 11 | 10 | rspcev 3622 | . . . . . . . . . 10
⊢ ((𝑔 ∈ 𝑋 ∧ (𝑔‘𝑥) ∈ ran 𝑔) → ∃𝑓 ∈ 𝑋 (𝑔‘𝑥) ∈ ran 𝑓) | 
| 12 | 5, 8, 11 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → ∃𝑓 ∈ 𝑋 (𝑔‘𝑥) ∈ ran 𝑓) | 
| 13 |  | eliun 4995 | . . . . . . . . 9
⊢ ((𝑔‘𝑥) ∈ ∪
𝑓 ∈ 𝑋 ran 𝑓 ↔ ∃𝑓 ∈ 𝑋 (𝑔‘𝑥) ∈ ran 𝑓) | 
| 14 | 12, 13 | sylibr 234 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ∪
𝑓 ∈ 𝑋 ran 𝑓) | 
| 15 |  | rnuni 6168 | . . . . . . . 8
⊢ ran ∪ 𝑋 =
∪ 𝑓 ∈ 𝑋 ran 𝑓 | 
| 16 | 14, 15 | eleqtrrdi 2852 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ran ∪
𝑋) | 
| 17 | 16 | ralrimiva 3146 | . . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ ran ∪
𝑋) | 
| 18 | 4, 17 | jca 511 | . . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → (𝑔 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ ran ∪
𝑋)) | 
| 19 |  | ffnfv 7139 | . . . . 5
⊢ (𝑔:𝐴⟶ran ∪
𝑋 ↔ (𝑔 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ ran ∪
𝑋)) | 
| 20 | 18, 19 | sylibr 234 | . . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔:𝐴⟶ran ∪
𝑋) | 
| 21 |  | ovexd 7466 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 ↑m 𝐴) ∈ V) | 
| 22 | 21, 1 | ssexd 5324 | . . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ V) | 
| 23 | 22 | uniexd 7762 | . . . . . . 7
⊢ (𝜑 → ∪ 𝑋
∈ V) | 
| 24 |  | rnexg 7924 | . . . . . . 7
⊢ (∪ 𝑋
∈ V → ran ∪ 𝑋 ∈ V) | 
| 25 | 23, 24 | syl 17 | . . . . . 6
⊢ (𝜑 → ran ∪ 𝑋
∈ V) | 
| 26 |  | unirnmap.a | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 27 | 25, 26 | elmapd 8880 | . . . . 5
⊢ (𝜑 → (𝑔 ∈ (ran ∪
𝑋 ↑m 𝐴) ↔ 𝑔:𝐴⟶ran ∪
𝑋)) | 
| 28 | 27 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → (𝑔 ∈ (ran ∪
𝑋 ↑m 𝐴) ↔ 𝑔:𝐴⟶ran ∪
𝑋)) | 
| 29 | 20, 28 | mpbird 257 | . . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔 ∈ (ran ∪
𝑋 ↑m 𝐴)) | 
| 30 | 29 | ralrimiva 3146 | . 2
⊢ (𝜑 → ∀𝑔 ∈ 𝑋 𝑔 ∈ (ran ∪
𝑋 ↑m 𝐴)) | 
| 31 |  | dfss3 3972 | . 2
⊢ (𝑋 ⊆ (ran ∪ 𝑋
↑m 𝐴)
↔ ∀𝑔 ∈
𝑋 𝑔 ∈ (ran ∪
𝑋 ↑m 𝐴)) | 
| 32 | 30, 31 | sylibr 234 | 1
⊢ (𝜑 → 𝑋 ⊆ (ran ∪
𝑋 ↑m 𝐴)) |