elpmi - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > elpmi		Structured version Visualization version GIF version

Theorem elpmi 7861

Description: A partial function is a function. (Contributed by Mario Carneiro, 15-Sep-2015.)

**Assertion**
Ref	Expression
elpmi	⊢ (𝐹 ∈ (𝐴 ↑_pm 𝐵) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵))

**Proof of Theorem elpmi**
Step	Hyp	Ref	Expression
1		n0i 3912	. . . 4 ⊢ (𝐹 ∈ (𝐴 ↑_pm 𝐵) → ¬ (𝐴 ↑_pm 𝐵) = ∅)
2		fnpm 7850	. . . . . 6 ⊢ ↑_pm Fn (V × V)
3		fndm 5978	. . . . . 6 ⊢ ( ↑_pm Fn (V × V) → dom ↑_pm = (V × V))
4	2, 3	ax-mp 5	. . . . 5 ⊢ dom ↑_pm = (V × V)
5	4	ndmov 6803	. . . 4 ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ↑_pm 𝐵) = ∅)
6	1, 5	nsyl2 142	. . 3 ⊢ (𝐹 ∈ (𝐴 ↑_pm 𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
7		elpm2g 7859	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐹 ∈ (𝐴 ↑_pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)))
8	6, 7	syl 17	. 2 ⊢ (𝐹 ∈ (𝐴 ↑_pm 𝐵) → (𝐹 ∈ (𝐴 ↑_pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)))
9	8	ibi 256	1 ⊢ (𝐹 ∈ (𝐴 ↑_pm 𝐵) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1481 ∈ wcel 1988 Vcvv 3195 ⊆ wss 3567 ∅c0 3907 × cxp 5102 dom cdm 5104 Fn wfn 5871 ⟶wf 5872 (class class class)co 6635 ↑_pm cpm 7843

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1720 ax-4 1735 ax-5 1837 ax-6 1886 ax-7 1933 ax-8 1990 ax-9 1997 ax-10 2017 ax-11 2032 ax-12 2045 ax-13 2244 ax-ext 2600 ax-sep 4772 ax-nul 4780 ax-pow 4834 ax-pr 4897 ax-un 6934

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1038 df-tru 1484 df-ex 1703 df-nf 1708 df-sb 1879 df-eu 2472 df-mo 2473 df-clab 2607 df-cleq 2613 df-clel 2616 df-nfc 2751 df-ne 2792 df-ral 2914 df-rex 2915 df-rab 2918 df-v 3197 df-sbc 3430 df-csb 3527 df-dif 3570 df-un 3572 df-in 3574 df-ss 3581 df-nul 3908 df-if 4078 df-pw 4151 df-sn 4169 df-pr 4171 df-op 4175 df-uni 4428 df-iun 4513 df-br 4645 df-opab 4704 df-mpt 4721 df-id 5014 df-xp 5110 df-rel 5111 df-cnv 5112 df-co 5113 df-dm 5114 df-rn 5115 df-res 5116 df-ima 5117 df-iota 5839 df-fun 5878 df-fn 5879 df-f 5880 df-fv 5884 df-ov 6638 df-oprab 6639 df-mpt2 6640 df-1st 7153 df-2nd 7154 df-pm 7845

This theorem is referenced by: pmfun 7862 pmresg 7870 equivcau 23079 dvn2bss 23674 mrsubff 31383 mrsubrn 31384 elpmrn 39230 elpmi2 39234 issmflem 40699

W3C validator