| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > fvssunirng | GIF version | ||
| Description: The result of a function value is always a subset of the union of the range, if the input is a set. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 24-May-2019.) |
| Ref | Expression |
|---|---|
| fvssunirng | ⊢ (𝐴 ∈ V → (𝐹‘𝐴) ⊆ ∪ ran 𝐹) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex 2776 | . . . . 5 ⊢ 𝑥 ∈ V | |
| 2 | brelrng 4917 | . . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝑥 ∈ V ∧ 𝐴𝐹𝑥) → 𝑥 ∈ ran 𝐹) | |
| 3 | 2 | 3exp 1205 | . . . . 5 ⊢ (𝐴 ∈ V → (𝑥 ∈ V → (𝐴𝐹𝑥 → 𝑥 ∈ ran 𝐹))) |
| 4 | 1, 3 | mpi 15 | . . . 4 ⊢ (𝐴 ∈ V → (𝐴𝐹𝑥 → 𝑥 ∈ ran 𝐹)) |
| 5 | elssuni 3883 | . . . 4 ⊢ (𝑥 ∈ ran 𝐹 → 𝑥 ⊆ ∪ ran 𝐹) | |
| 6 | 4, 5 | syl6 33 | . . 3 ⊢ (𝐴 ∈ V → (𝐴𝐹𝑥 → 𝑥 ⊆ ∪ ran 𝐹)) |
| 7 | 6 | alrimiv 1898 | . 2 ⊢ (𝐴 ∈ V → ∀𝑥(𝐴𝐹𝑥 → 𝑥 ⊆ ∪ ran 𝐹)) |
| 8 | fvss 5602 | . 2 ⊢ (∀𝑥(𝐴𝐹𝑥 → 𝑥 ⊆ ∪ ran 𝐹) → (𝐹‘𝐴) ⊆ ∪ ran 𝐹) | |
| 9 | 7, 8 | syl 14 | 1 ⊢ (𝐴 ∈ V → (𝐹‘𝐴) ⊆ ∪ ran 𝐹) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∀wal 1371 ∈ wcel 2177 Vcvv 2773 ⊆ wss 3170 ∪ cuni 3855 class class class wbr 4050 ran crn 4683 ‘cfv 5279 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-14 2180 ax-ext 2188 ax-sep 4169 ax-pow 4225 ax-pr 4260 |
| This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ral 2490 df-rex 2491 df-v 2775 df-un 3174 df-in 3176 df-ss 3183 df-pw 3622 df-sn 3643 df-pr 3644 df-op 3646 df-uni 3856 df-br 4051 df-opab 4113 df-cnv 4690 df-dm 4692 df-rn 4693 df-iota 5240 df-fv 5287 |
| This theorem is referenced by: fvexg 5607 ovssunirng 5991 strfvssn 12924 ptex 13166 prdsvallem 13174 prdsval 13175 xmetunirn 14900 mopnval 14984 |
| Copyright terms: Public domain | W3C validator |