Theorem bj-imdirval2lem

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

	Ref	Expression
Hypotheses	bj-imdirval2lem.exa	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	bj-imdirval2lem.exb	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
Assertion	bj-imdirval2lem	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ 𝜓 ) } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		bj-imdirval2lem.exa	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
2		bj-imdirval2lem.exb	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3	1	pwexd	⊢ ( 𝜑 → 𝒫 𝐴 ∈ V )
4	2	pwexd	⊢ ( 𝜑 → 𝒫 𝐵 ∈ V )
5		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ) → 𝑥 ⊆ 𝐴 )
6		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
7	5 6	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ) → 𝑥 ∈ 𝒫 𝐴 )
8		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ) → 𝑦 ⊆ 𝐵 )
9		velpw	⊢ ( 𝑦 ∈ 𝒫 𝐵 ↔ 𝑦 ⊆ 𝐵 )
10	8 9	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ) → 𝑦 ∈ 𝒫 𝐵 )
11	3 4 7 10	opabex2	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) } ∈ V )
12		simpl	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ 𝜓 ) → ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) )
13	12	ssopab2i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ 𝜓 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) }
14	13	a1i	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ 𝜓 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) } )
15	11 14	ssexd	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ 𝜓 ) } ∈ V )