| Step | Hyp | Ref
| Expression |
| 1 | | unirnmapsn.C |
. . . . 5
⊢ 𝐶 = {𝐴} |
| 2 | | snex 5436 |
. . . . 5
⊢ {𝐴} ∈ V |
| 3 | 1, 2 | eqeltri 2837 |
. . . 4
⊢ 𝐶 ∈ V |
| 4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐶 ∈ V) |
| 5 | | unirnmapsn.x |
. . 3
⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑m 𝐶)) |
| 6 | 4, 5 | unirnmap 45213 |
. 2
⊢ (𝜑 → 𝑋 ⊆ (ran ∪
𝑋 ↑m 𝐶)) |
| 7 | | simpl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋 ↑m 𝐶)) → 𝜑) |
| 8 | | equid 2011 |
. . . . . . 7
⊢ 𝑔 = 𝑔 |
| 9 | | rnuni 6168 |
. . . . . . . 8
⊢ ran ∪ 𝑋 =
∪ 𝑓 ∈ 𝑋 ran 𝑓 |
| 10 | 9 | oveq1i 7441 |
. . . . . . 7
⊢ (ran
∪ 𝑋 ↑m 𝐶) = (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶) |
| 11 | 8, 10 | eleq12i 2834 |
. . . . . 6
⊢ (𝑔 ∈ (ran ∪ 𝑋
↑m 𝐶)
↔ 𝑔 ∈ (∪ 𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶)) |
| 12 | 11 | biimpi 216 |
. . . . 5
⊢ (𝑔 ∈ (ran ∪ 𝑋
↑m 𝐶)
→ 𝑔 ∈ (∪ 𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶)) |
| 13 | 12 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋 ↑m 𝐶)) → 𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶)) |
| 14 | | ovexd 7466 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ↑m 𝐶) ∈ V) |
| 15 | 14, 5 | ssexd 5324 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ V) |
| 16 | | rnexg 7924 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝑋 → ran 𝑓 ∈ V) |
| 17 | 16 | rgen 3063 |
. . . . . . . . . 10
⊢
∀𝑓 ∈
𝑋 ran 𝑓 ∈ V |
| 18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑓 ∈ 𝑋 ran 𝑓 ∈ V) |
| 19 | | iunexg 7988 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ ∀𝑓 ∈ 𝑋 ran 𝑓 ∈ V) → ∪ 𝑓 ∈ 𝑋 ran 𝑓 ∈ V) |
| 20 | 15, 18, 19 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑓 ∈ 𝑋 ran 𝑓 ∈ V) |
| 21 | 20, 4 | elmapd 8880 |
. . . . . . 7
⊢ (𝜑 → (𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶) ↔ 𝑔:𝐶⟶∪
𝑓 ∈ 𝑋 ran 𝑓)) |
| 22 | 21 | biimpa 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶)) → 𝑔:𝐶⟶∪
𝑓 ∈ 𝑋 ran 𝑓) |
| 23 | | unirnmapsn.A |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 24 | | snidg 4660 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
| 25 | 23, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
| 26 | 25, 1 | eleqtrrdi 2852 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝐶) |
| 27 | 26 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶)) → 𝐴 ∈ 𝐶) |
| 28 | 22, 27 | ffvelcdmd 7105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶)) → (𝑔‘𝐴) ∈ ∪
𝑓 ∈ 𝑋 ran 𝑓) |
| 29 | | eliun 4995 |
. . . . 5
⊢ ((𝑔‘𝐴) ∈ ∪
𝑓 ∈ 𝑋 ran 𝑓 ↔ ∃𝑓 ∈ 𝑋 (𝑔‘𝐴) ∈ ran 𝑓) |
| 30 | 28, 29 | sylib 218 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ (∪
𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶)) → ∃𝑓 ∈ 𝑋 (𝑔‘𝐴) ∈ ran 𝑓) |
| 31 | 7, 13, 30 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋 ↑m 𝐶)) → ∃𝑓 ∈ 𝑋 (𝑔‘𝐴) ∈ ran 𝑓) |
| 32 | | elmapfn 8905 |
. . . . . 6
⊢ (𝑔 ∈ (ran ∪ 𝑋
↑m 𝐶)
→ 𝑔 Fn 𝐶) |
| 33 | 32 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋 ↑m 𝐶)) → 𝑔 Fn 𝐶) |
| 34 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → (𝑔‘𝐴) ∈ ran 𝑓) |
| 35 | 23 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝐴 ∈ 𝑉) |
| 36 | 1 | oveq2i 7442 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ↑m 𝐶) = (𝐵 ↑m {𝐴}) |
| 37 | 5, 36 | sseqtrdi 4024 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑m {𝐴})) |
| 38 | 37 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑋 ⊆ (𝐵 ↑m {𝐴})) |
| 39 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ 𝑋) |
| 40 | 38, 39 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ (𝐵 ↑m {𝐴})) |
| 41 | | unirnmapsn.b |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
| 42 | 41 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝐵 ∈ 𝑊) |
| 43 | 2 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → {𝐴} ∈ V) |
| 44 | 42, 43 | elmapd 8880 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑓 ∈ (𝐵 ↑m {𝐴}) ↔ 𝑓:{𝐴}⟶𝐵)) |
| 45 | 40, 44 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓:{𝐴}⟶𝐵) |
| 46 | 45 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝑓:{𝐴}⟶𝐵) |
| 47 | 35, 46 | rnsnf 45189 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → ran 𝑓 = {(𝑓‘𝐴)}) |
| 48 | 34, 47 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → (𝑔‘𝐴) ∈ {(𝑓‘𝐴)}) |
| 49 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝑔‘𝐴) ∈ V |
| 50 | 49 | elsn 4641 |
. . . . . . . . . 10
⊢ ((𝑔‘𝐴) ∈ {(𝑓‘𝐴)} ↔ (𝑔‘𝐴) = (𝑓‘𝐴)) |
| 51 | 48, 50 | sylib 218 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → (𝑔‘𝐴) = (𝑓‘𝐴)) |
| 52 | 51 | 3adant1r 1178 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → (𝑔‘𝐴) = (𝑓‘𝐴)) |
| 53 | 23 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 Fn 𝐶) → 𝐴 ∈ 𝑉) |
| 54 | 53 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝐴 ∈ 𝑉) |
| 55 | | simp1r 1199 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝑔 Fn 𝐶) |
| 56 | 40, 36 | eleqtrrdi 2852 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ (𝐵 ↑m 𝐶)) |
| 57 | | elmapfn 8905 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (𝐵 ↑m 𝐶) → 𝑓 Fn 𝐶) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 Fn 𝐶) |
| 59 | 58 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋) → 𝑓 Fn 𝐶) |
| 60 | 59 | 3adant3 1133 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝑓 Fn 𝐶) |
| 61 | 54, 1, 55, 60 | fsneq 45211 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → (𝑔 = 𝑓 ↔ (𝑔‘𝐴) = (𝑓‘𝐴))) |
| 62 | 52, 61 | mpbird 257 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝑔 = 𝑓) |
| 63 | | simp2 1138 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝑓 ∈ 𝑋) |
| 64 | 62, 63 | eqeltrd 2841 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Fn 𝐶) ∧ 𝑓 ∈ 𝑋 ∧ (𝑔‘𝐴) ∈ ran 𝑓) → 𝑔 ∈ 𝑋) |
| 65 | 64 | 3exp 1120 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 Fn 𝐶) → (𝑓 ∈ 𝑋 → ((𝑔‘𝐴) ∈ ran 𝑓 → 𝑔 ∈ 𝑋))) |
| 66 | 7, 33, 65 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋 ↑m 𝐶)) → (𝑓 ∈ 𝑋 → ((𝑔‘𝐴) ∈ ran 𝑓 → 𝑔 ∈ 𝑋))) |
| 67 | 66 | rexlimdv 3153 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋 ↑m 𝐶)) → (∃𝑓 ∈ 𝑋 (𝑔‘𝐴) ∈ ran 𝑓 → 𝑔 ∈ 𝑋)) |
| 68 | 31, 67 | mpd 15 |
. 2
⊢ ((𝜑 ∧ 𝑔 ∈ (ran ∪
𝑋 ↑m 𝐶)) → 𝑔 ∈ 𝑋) |
| 69 | 6, 68 | eqelssd 4005 |
1
⊢ (𝜑 → 𝑋 = (ran ∪ 𝑋 ↑m 𝐶)) |