Step | Hyp | Ref
| Expression |
1 | | unirnmap.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑𝑚 𝐴)) |
2 | 1 | sselda 3568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔 ∈ (𝐵 ↑𝑚 𝐴)) |
3 | | elmapfn 7766 |
. . . . . . 7
⊢ (𝑔 ∈ (𝐵 ↑𝑚 𝐴) → 𝑔 Fn 𝐴) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔 Fn 𝐴) |
5 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ 𝑋) |
6 | | dffn3 5967 |
. . . . . . . . . . . 12
⊢ (𝑔 Fn 𝐴 ↔ 𝑔:𝐴⟶ran 𝑔) |
7 | 4, 6 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔:𝐴⟶ran 𝑔) |
8 | 7 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ran 𝑔) |
9 | | rneq 5272 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → ran 𝑓 = ran 𝑔) |
10 | 9 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ((𝑔‘𝑥) ∈ ran 𝑓 ↔ (𝑔‘𝑥) ∈ ran 𝑔)) |
11 | 10 | rspcev 3282 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ 𝑋 ∧ (𝑔‘𝑥) ∈ ran 𝑔) → ∃𝑓 ∈ 𝑋 (𝑔‘𝑥) ∈ ran 𝑓) |
12 | 5, 8, 11 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → ∃𝑓 ∈ 𝑋 (𝑔‘𝑥) ∈ ran 𝑓) |
13 | | eliun 4460 |
. . . . . . . . 9
⊢ ((𝑔‘𝑥) ∈ ∪
𝑓 ∈ 𝑋 ran 𝑓 ↔ ∃𝑓 ∈ 𝑋 (𝑔‘𝑥) ∈ ran 𝑓) |
14 | 12, 13 | sylibr 223 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ∪
𝑓 ∈ 𝑋 ran 𝑓) |
15 | | rnuni 5463 |
. . . . . . . 8
⊢ ran ∪ 𝑋 =
∪ 𝑓 ∈ 𝑋 ran 𝑓 |
16 | 14, 15 | syl6eleqr 2699 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ran ∪
𝑋) |
17 | 16 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ ran ∪
𝑋) |
18 | 4, 17 | jca 553 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → (𝑔 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ ran ∪
𝑋)) |
19 | | ffnfv 6295 |
. . . . 5
⊢ (𝑔:𝐴⟶ran ∪
𝑋 ↔ (𝑔 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ ran ∪
𝑋)) |
20 | 18, 19 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔:𝐴⟶ran ∪
𝑋) |
21 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝐵 ↑𝑚
𝐴) ∈
V |
22 | 21 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ↑𝑚 𝐴) ∈ V) |
23 | 22, 1 | ssexd 4733 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ V) |
24 | | uniexg 6853 |
. . . . . . . 8
⊢ (𝑋 ∈ V → ∪ 𝑋
∈ V) |
25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑋
∈ V) |
26 | | rnexg 6990 |
. . . . . . 7
⊢ (∪ 𝑋
∈ V → ran ∪ 𝑋 ∈ V) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran ∪ 𝑋
∈ V) |
28 | | unirnmap.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
29 | 27, 28 | elmapd 7758 |
. . . . 5
⊢ (𝜑 → (𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐴) ↔ 𝑔:𝐴⟶ran ∪
𝑋)) |
30 | 29 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → (𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐴) ↔ 𝑔:𝐴⟶ran ∪
𝑋)) |
31 | 20, 30 | mpbird 246 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑋) → 𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐴)) |
32 | 31 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑔 ∈ 𝑋 𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐴)) |
33 | | dfss3 3558 |
. 2
⊢ (𝑋 ⊆ (ran ∪ 𝑋
↑𝑚 𝐴) ↔ ∀𝑔 ∈ 𝑋 𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐴)) |
34 | 32, 33 | sylibr 223 |
1
⊢ (𝜑 → 𝑋 ⊆ (ran ∪
𝑋
↑𝑚 𝐴)) |