Step | Hyp | Ref
| Expression |
1 | | unirnmap.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑𝑚 𝐴)) |
2 | 1 | sselda 3857 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔 ∈ (𝐵 ↑𝑚 𝐴)) |
3 | | elmapfn 8225 |
. . . . . . 7
⊢ (𝑔 ∈ (𝐵 ↑𝑚 𝐴) → 𝑔 Fn 𝐴) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔 Fn 𝐴) |
5 | | simplr 756 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ 𝑋) |
6 | | dffn3 6353 |
. . . . . . . . . . . 12
⊢ (𝑔 Fn 𝐴 ↔ 𝑔:𝐴⟶ran 𝑔) |
7 | 4, 6 | sylib 210 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔:𝐴⟶ran 𝑔) |
8 | 7 | ffvelrnda 6674 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ran 𝑔) |
9 | | rneq 5646 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → ran 𝑓 = ran 𝑔) |
10 | 9 | eleq2d 2848 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ((𝑔‘𝑥) ∈ ran 𝑓 ↔ (𝑔‘𝑥) ∈ ran 𝑔)) |
11 | 10 | rspcev 3532 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ 𝑋 ∧ (𝑔‘𝑥) ∈ ran 𝑔) → ∃𝑓 ∈ 𝑋 (𝑔‘𝑥) ∈ ran 𝑓) |
12 | 5, 8, 11 | syl2anc 576 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → ∃𝑓 ∈ 𝑋 (𝑔‘𝑥) ∈ ran 𝑓) |
13 | | eliun 4794 |
. . . . . . . . 9
⊢ ((𝑔‘𝑥) ∈ ∪
𝑓 ∈ 𝑋 ran 𝑓 ↔ ∃𝑓 ∈ 𝑋 (𝑔‘𝑥) ∈ ran 𝑓) |
14 | 12, 13 | sylibr 226 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ∪
𝑓 ∈ 𝑋 ran 𝑓) |
15 | | rnuni 5845 |
. . . . . . . 8
⊢ ran ∪ 𝑋 =
∪ 𝑓 ∈ 𝑋 ran 𝑓 |
16 | 14, 15 | syl6eleqr 2874 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ran ∪
𝑋) |
17 | 16 | ralrimiva 3129 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ ran ∪
𝑋) |
18 | 4, 17 | jca 504 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → (𝑔 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ ran ∪
𝑋)) |
19 | | ffnfv 6703 |
. . . . 5
⊢ (𝑔:𝐴⟶ran ∪
𝑋 ↔ (𝑔 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ ran ∪
𝑋)) |
20 | 18, 19 | sylibr 226 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔:𝐴⟶ran ∪
𝑋) |
21 | | ovexd 7008 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ↑𝑚 𝐴) ∈ V) |
22 | 21, 1 | ssexd 5082 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ V) |
23 | | uniexg 7283 |
. . . . . . . 8
⊢ (𝑋 ∈ V → ∪ 𝑋
∈ V) |
24 | 22, 23 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑋
∈ V) |
25 | | rnexg 7427 |
. . . . . . 7
⊢ (∪ 𝑋
∈ V → ran ∪ 𝑋 ∈ V) |
26 | 24, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran ∪ 𝑋
∈ V) |
27 | | unirnmap.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
28 | 26, 27 | elmapd 8216 |
. . . . 5
⊢ (𝜑 → (𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐴) ↔ 𝑔:𝐴⟶ran ∪
𝑋)) |
29 | 28 | adantr 473 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → (𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐴) ↔ 𝑔:𝐴⟶ran ∪
𝑋)) |
30 | 20, 29 | mpbird 249 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐴)) |
31 | 30 | ralrimiva 3129 |
. 2
⊢ (𝜑 → ∀𝑔 ∈ 𝑋 𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐴)) |
32 | | dfss3 3846 |
. 2
⊢ (𝑋 ⊆ (ran ∪ 𝑋
↑𝑚 𝐴) ↔ ∀𝑔 ∈ 𝑋 𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐴)) |
33 | 31, 32 | sylibr 226 |
1
⊢ (𝜑 → 𝑋 ⊆ (ran ∪
𝑋
↑𝑚 𝐴)) |