Step | Hyp | Ref
| Expression |
1 | | unirnmapsn.C |
. . . . 5
⊢ 𝐶 = {𝐴} |
2 | | snex 4835 |
. . . . 5
⊢ {𝐴} ∈ V |
3 | 1, 2 | eqeltri 2684 |
. . . 4
⊢ 𝐶 ∈ V |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐶 ∈ V) |
5 | | unirnmapsn.x |
. . 3
⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑𝑚 𝐶)) |
6 | 4, 5 | unirnmap 38395 |
. 2
⊢ (𝜑 → 𝑋 ⊆ (ran ∪
𝑋
↑𝑚 𝐶)) |
7 | | simpl 472 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐶)) → 𝜑) |
8 | | equid 1926 |
. . . . . . . . 9
⊢ 𝑔 = 𝑔 |
9 | | rnuni 5463 |
. . . . . . . . . 10
⊢ ran ∪ 𝑋 =
∪ 𝑓 ∈ 𝑋 ran 𝑓 |
10 | 9 | oveq1i 6559 |
. . . . . . . . 9
⊢ (ran
∪ 𝑋 ↑𝑚 𝐶) = (∪ 𝑓 ∈ 𝑋 ran 𝑓 ↑𝑚 𝐶) |
11 | 8, 10 | eleq12i 2681 |
. . . . . . . 8
⊢ (𝑔 ∈ (ran ∪ 𝑋
↑𝑚 𝐶) ↔ 𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑𝑚 𝐶)) |
12 | 11 | biimpi 205 |
. . . . . . 7
⊢ (𝑔 ∈ (ran ∪ 𝑋
↑𝑚 𝐶) → 𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑𝑚 𝐶)) |
13 | 12 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐶)) → 𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑𝑚 𝐶)) |
14 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝐵 ↑𝑚
𝐶) ∈
V |
15 | 14 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ↑𝑚 𝐶) ∈ V) |
16 | 15, 5 | ssexd 4733 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ V) |
17 | | rnexg 6990 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ 𝑋 → ran 𝑓 ∈ V) |
18 | 17 | rgen 2906 |
. . . . . . . . . . . 12
⊢
∀𝑓 ∈
𝑋 ran 𝑓 ∈ V |
19 | 18 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑓 ∈ 𝑋 ran 𝑓 ∈ V) |
20 | | iunexg 7035 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ ∀𝑓 ∈ 𝑋 ran 𝑓 ∈ V) → ∪ 𝑓 ∈ 𝑋 ran 𝑓 ∈ V) |
21 | 16, 19, 20 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑓 ∈ 𝑋 ran 𝑓 ∈ V) |
22 | 21, 4 | elmapd 7758 |
. . . . . . . . 9
⊢ (𝜑 → (𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑𝑚 𝐶) ↔ 𝑔:𝐶⟶∪
𝑓 ∈ 𝑋 ran 𝑓)) |
23 | 22 | biimpa 500 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑𝑚 𝐶)) → 𝑔:𝐶⟶∪
𝑓 ∈ 𝑋 ran 𝑓) |
24 | | unirnmapsn.A |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
25 | | snidg 4153 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
27 | 26, 1 | syl6eleqr 2699 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝐶) |
28 | 27 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑𝑚 𝐶)) → 𝐴 ∈ 𝐶) |
29 | 23, 28 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑𝑚 𝐶)) → (𝑔‘𝐴) ∈ ∪
𝑓 ∈ 𝑋 ran 𝑓) |
30 | | eliun 4460 |
. . . . . . 7
⊢ ((𝑔‘𝐴) ∈ ∪
𝑓 ∈ 𝑋 ran 𝑓 ↔ ∃𝑓 ∈ 𝑋 (𝑔‘𝐴) ∈ ran 𝑓) |
31 | 29, 30 | sylib 207 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑𝑚 𝐶)) → ∃𝑓 ∈ 𝑋 (𝑔‘𝐴) ∈ ran 𝑓) |
32 | 7, 13, 31 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐶)) → ∃𝑓 ∈ 𝑋 (𝑔‘𝐴) ∈ ran 𝑓) |
33 | | elmapfn 7766 |
. . . . . . . 8
⊢ (𝑔 ∈ (ran ∪ 𝑋
↑𝑚 𝐶) → 𝑔 Fn 𝐶) |
34 | 33 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐶)) → 𝑔 Fn 𝐶) |
35 | | simp3 1056 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → (𝑔‘𝐴) ∈ ran 𝑓) |
36 | 24 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝐴 ∈ 𝑉) |
37 | 1 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ↑𝑚
𝐶) = (𝐵 ↑𝑚 {𝐴}) |
38 | 5, 37 | syl6sseq 3614 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑𝑚 {𝐴})) |
39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑋 ⊆ (𝐵 ↑𝑚 {𝐴})) |
40 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ 𝑋) |
41 | 39, 40 | sseldd 3569 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ (𝐵 ↑𝑚 {𝐴})) |
42 | | unirnmapsn.b |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
43 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝐵 ∈ 𝑊) |
44 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → {𝐴} ∈ V) |
45 | 43, 44 | elmapd 7758 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑓 ∈ (𝐵 ↑𝑚 {𝐴}) ↔ 𝑓:{𝐴}⟶𝐵)) |
46 | 41, 45 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓:{𝐴}⟶𝐵) |
47 | 46 | 3adant3 1074 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝑓:{𝐴}⟶𝐵) |
48 | 36, 47 | rnsnf 38365 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → ran 𝑓 = {(𝑓‘𝐴)}) |
49 | 35, 48 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → (𝑔‘𝐴) ∈ {(𝑓‘𝐴)}) |
50 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝑔‘𝐴) ∈ V |
51 | 50 | elsn 4140 |
. . . . . . . . . . . 12
⊢ ((𝑔‘𝐴) ∈ {(𝑓‘𝐴)} ↔ (𝑔‘𝐴) = (𝑓‘𝐴)) |
52 | 49, 51 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → (𝑔‘𝐴) = (𝑓‘𝐴)) |
53 | 52 | 3adant1r 1311 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → (𝑔‘𝐴) = (𝑓‘𝐴)) |
54 | 24 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 Fn 𝐶) → 𝐴 ∈ 𝑉) |
55 | 54 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝐴 ∈ 𝑉) |
56 | | simp1r 1079 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝑔 Fn 𝐶) |
57 | 41, 37 | syl6eleqr 2699 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ (𝐵 ↑𝑚 𝐶)) |
58 | | elmapfn 7766 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (𝐵 ↑𝑚 𝐶) → 𝑓 Fn 𝐶) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 Fn 𝐶) |
60 | 59 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋) → 𝑓 Fn 𝐶) |
61 | 60 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝑓 Fn 𝐶) |
62 | 55, 1, 56, 61 | fsneq 38393 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → (𝑔 = 𝑓 ↔ (𝑔‘𝐴) = (𝑓‘𝐴))) |
63 | 53, 62 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝑔 = 𝑓) |
64 | | simp2 1055 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝑓 ∈ 𝑋) |
65 | 63, 64 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝑔 ∈ 𝑋) |
66 | 65 | 3exp 1256 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 Fn 𝐶) → (𝑓 ∈ 𝑋 → ((𝑔‘𝐴) ∈ ran 𝑓 → 𝑔 ∈ 𝑋))) |
67 | 7, 34, 66 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐶)) → (𝑓 ∈ 𝑋 → ((𝑔‘𝐴) ∈ ran 𝑓 → 𝑔 ∈ 𝑋))) |
68 | 67 | rexlimdv 3012 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐶)) → (∃𝑓 ∈ 𝑋 (𝑔‘𝐴) ∈ ran 𝑓 → 𝑔 ∈ 𝑋)) |
69 | 32, 68 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐶)) → 𝑔 ∈ 𝑋) |
70 | 69 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐶)𝑔 ∈ 𝑋) |
71 | | dfss3 3558 |
. . 3
⊢ ((ran
∪ 𝑋 ↑𝑚 𝐶) ⊆ 𝑋 ↔ ∀𝑔 ∈ (ran ∪
𝑋
↑𝑚 𝐶)𝑔 ∈ 𝑋) |
72 | 70, 71 | sylibr 223 |
. 2
⊢ (𝜑 → (ran ∪ 𝑋
↑𝑚 𝐶) ⊆ 𝑋) |
73 | 6, 72 | eqssd 3585 |
1
⊢ (𝜑 → 𝑋 = (ran ∪ 𝑋 ↑𝑚
𝐶)) |