Theorem bj-imdirvallem

Description: Lemma for bj-imdirval and bj-iminvval . (Contributed by BJ, 23-May-2024)

	Ref	Expression
Hypotheses	bj-imdirvallem.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	bj-imdirvallem.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	bj-imdirvallem.df	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ 𝜓 ) } ) )
Assertion	bj-imdirvallem	⊢ ( 𝜑 → ( 𝐴 𝐶 𝐵 ) = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ 𝜓 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		bj-imdirvallem.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
2		bj-imdirvallem.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3		bj-imdirvallem.df	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ 𝜓 ) } ) )
4	3	a1i	⊢ ( 𝜑 → 𝐶 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ 𝜓 ) } ) ) )
5		xpeq12	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 × 𝑏 ) = ( 𝐴 × 𝐵 ) )
6	5	pweqd	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → 𝒫 ( 𝑎 × 𝑏 ) = 𝒫 ( 𝐴 × 𝐵 ) )
7	6	adantl	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → 𝒫 ( 𝑎 × 𝑏 ) = 𝒫 ( 𝐴 × 𝐵 ) )
8		sseq2	⊢ ( 𝑎 = 𝐴 → ( 𝑥 ⊆ 𝑎 ↔ 𝑥 ⊆ 𝐴 ) )
9		sseq2	⊢ ( 𝑏 = 𝐵 → ( 𝑦 ⊆ 𝑏 ↔ 𝑦 ⊆ 𝐵 ) )
10	8 9	bi2anan9	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ) )
11	10	anbi1d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ 𝜓 ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ 𝜓 ) ) )
12	11	opabbidv	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ 𝜓 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ 𝜓 ) } )
13	12	adantl	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ 𝜓 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ 𝜓 ) } )
14	7 13	mpteq12dv	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ 𝜓 ) } ) = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ 𝜓 ) } ) )
15	1	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
16	2	elexd	⊢ ( 𝜑 → 𝐵 ∈ V )
17	1 2	xpexd	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) ∈ V )
18	17	pwexd	⊢ ( 𝜑 → 𝒫 ( 𝐴 × 𝐵 ) ∈ V )
19	18	mptexd	⊢ ( 𝜑 → ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ 𝜓 ) } ) ∈ V )
20	4 14 15 16 19	ovmpod	⊢ ( 𝜑 → ( 𝐴 𝐶 𝐵 ) = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ 𝜓 ) } ) )