Theorem fsovd 43742

Description: Value of the operator, (𝐴𝑂𝐵), which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, 𝐴 and 𝐵. (Contributed by RP, 25-Apr-2021.)

Hypotheses

Ref	Expression
fsovd.fs	⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
fsovd.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
fsovd.b	⊢ (𝜑 → 𝐵 ∈ 𝑊)

Assertion

Ref	Expression
fsovd	⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))

Distinct variable groups:   𝐴,𝑎,𝑏,𝑓   𝑥,𝐴,𝑎,𝑏   𝑦,𝐴,𝑎,𝑏   𝐵,𝑎,𝑏,𝑓   𝑦,𝐵   𝜑,𝑎,𝑏

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓)   𝐵(𝑥)   𝑂(𝑥,𝑦,𝑓,𝑎,𝑏)   𝑉(𝑥,𝑦,𝑓,𝑎,𝑏)   𝑊(𝑥,𝑦,𝑓,𝑎,𝑏)

Proof of Theorem fsovd

Step	Hyp	Ref	Expression
1		fsovd.fs	. . 3 ⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}))))
3		pweq 4622	. . . . . 6 ⊢ (𝑏 = 𝐵 → 𝒫 𝑏 = 𝒫 𝐵)
4	3	adantl 480	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 𝒫 𝑏 = 𝒫 𝐵)
5		simpl 481	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 𝑎 = 𝐴)
6	4, 5	oveq12d 7445	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝒫 𝑏 ↑m 𝑎) = (𝒫 𝐵 ↑m 𝐴))
7		simpr 483	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
8		rabeq 3443	. . . . . 6 ⊢ (𝑎 = 𝐴 → {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})
9	8	adantr 479	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})
10	7, 9	mpteq12dv 5245	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)}) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)}))
11	6, 10	mpteq12dv 5245	. . 3 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
12	11	adantl 480	. 2 ⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))
13		fsovd.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
14	13	elexd 3496	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
15		fsovd.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
16	15	elexd 3496	. 2 ⊢ (𝜑 → 𝐵 ∈ V)
17		ovex 7460	. . . 4 ⊢ (𝒫 𝐵 ↑m 𝐴) ∈ V
18	17	mptex 7242	. . 3 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})) ∈ V
19	18	a1i 11	. 2 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})) ∈ V)
20	2, 12, 14, 16, 19	ovmpod 7580	1 ⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∈ wcel 2100  {crab 3428  Vcvv 3472  𝒫 cpw 4608   ↦ cmpt 5237  ‘cfv 6556  (class class class)co 7427   ∈ cmpo 7429   ↑_m cmap 8859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-rep 5291  ax-sep 5305  ax-nul 5312  ax-pr 5435

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3788  df-csb 3904  df-dif 3961  df-un 3963  df-in 3965  df-ss 3975  df-nul 4334  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-iun 5006  df-br 5155  df-opab 5217  df-mpt 5238  df-id 5582  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-ov 7430  df-oprab 7431  df-mpo 7432

This theorem is referenced by:  fsovrfovd  43743  fsovfvd  43744  fsovfd  43746  fsovcnvlem  43747