bj-imdirval3

Description: Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023)

	Ref	Expression
Hypotheses	bj-imdirval3.exa	$⊢ φ \to A \in U$
	bj-imdirval3.exb	$⊢ φ \to B \in V$
	bj-imdirval3.arg	$⊢ φ \to R \subseteq A \times B$
Assertion	bj-imdirval3	$⊢ φ \to (X (A 𝒫_{*} B) (R) Y \leftrightarrow ((X \subseteq A \land Y \subseteq B) \land R [X] = Y))$

Proof

Step	Hyp	Ref	Expression
1		bj-imdirval3.exa	$⊢ φ \to A \in U$
2		bj-imdirval3.exb	$⊢ φ \to B \in V$
3		bj-imdirval3.arg	$⊢ φ \to R \subseteq A \times B$
4	1 2 3	bj-imdirval2	$⊢ φ \to (A 𝒫_{*} B) (R) = \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land R [x] = y)\}$
5	4	breqd	$⊢ φ \to (X (A 𝒫_{*} B) (R) Y \leftrightarrow X \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land R [x] = y)\} Y)$
6		brabv	$⊢ X \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land R [x] = y)\} Y \to (X \in V \land Y \in V)$
7	5 6	biimtrdi	$⊢ φ \to (X (A 𝒫_{*} B) (R) Y \to (X \in V \land Y \in V))$
8	7	pm4.71rd	$⊢ φ \to (X (A 𝒫_{} B) (R) Y \leftrightarrow ((X \in V \land Y \in V) \land X (A 𝒫_{} B) (R) Y))$
9		simpl	$⊢ (X \in V \land Y \in V) \to X \in V$
10	9	adantl	$⊢ (φ \land (X \in V \land Y \in V)) \to X \in V$
11		simpr	$⊢ (X \in V \land Y \in V) \to Y \in V$
12	11	adantl	$⊢ (φ \land (X \in V \land Y \in V)) \to Y \in V$
13	4	adantr	$⊢ (φ \land (X \in V \land Y \in V)) \to (A 𝒫_{*} B) (R) = \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land R [x] = y)\}$
14		simpl	$⊢ (x = X \land y = Y) \to x = X$
15	14	sseq1d	$⊢ (x = X \land y = Y) \to (x \subseteq A \leftrightarrow X \subseteq A)$
16		simpr	$⊢ (x = X \land y = Y) \to y = Y$
17	16	sseq1d	$⊢ (x = X \land y = Y) \to (y \subseteq B \leftrightarrow Y \subseteq B)$
18	15 17	anbi12d	$⊢ (x = X \land y = Y) \to ((x \subseteq A \land y \subseteq B) \leftrightarrow (X \subseteq A \land Y \subseteq B))$
19		imaeq2	$⊢ x = X \to R [x] = R [X]$
20		id	$⊢ y = Y \to y = Y$
21	19 20	eqeqan12d	$⊢ (x = X \land y = Y) \to (R [x] = y \leftrightarrow R [X] = Y)$
22	18 21	anbi12d	$⊢ (x = X \land y = Y) \to (((x \subseteq A \land y \subseteq B) \land R [x] = y) \leftrightarrow ((X \subseteq A \land Y \subseteq B) \land R [X] = Y))$
23	22	adantl	$⊢ ((φ \land (X \in V \land Y \in V)) \land (x = X \land y = Y)) \to (((x \subseteq A \land y \subseteq B) \land R [x] = y) \leftrightarrow ((X \subseteq A \land Y \subseteq B) \land R [X] = Y))$
24	10 12 13 23	brabd	$⊢ (φ \land (X \in V \land Y \in V)) \to (X (A 𝒫_{*} B) (R) Y \leftrightarrow ((X \subseteq A \land Y \subseteq B) \land R [X] = Y))$
25	24	pm5.32da	$⊢ φ \to (((X \in V \land Y \in V) \land X (A 𝒫_{*} B) (R) Y) \leftrightarrow ((X \in V \land Y \in V) \land ((X \subseteq A \land Y \subseteq B) \land R [X] = Y)))$
26		simpr	$⊢ ((X \in V \land Y \in V) \land ((X \subseteq A \land Y \subseteq B) \land R [X] = Y)) \to ((X \subseteq A \land Y \subseteq B) \land R [X] = Y)$
27	1	adantr	$⊢ (φ \land X \subseteq A) \to A \in U$
28		simpr	$⊢ (φ \land X \subseteq A) \to X \subseteq A$
29	27 28	ssexd	$⊢ (φ \land X \subseteq A) \to X \in V$
30	29	ex	$⊢ φ \to (X \subseteq A \to X \in V)$
31	2	adantr	$⊢ (φ \land Y \subseteq B) \to B \in V$
32		simpr	$⊢ (φ \land Y \subseteq B) \to Y \subseteq B$
33	31 32	ssexd	$⊢ (φ \land Y \subseteq B) \to Y \in V$
34	33	ex	$⊢ φ \to (Y \subseteq B \to Y \in V)$
35	30 34	anim12d	$⊢ φ \to ((X \subseteq A \land Y \subseteq B) \to (X \in V \land Y \in V))$
36	35	adantrd	$⊢ φ \to (((X \subseteq A \land Y \subseteq B) \land R [X] = Y) \to (X \in V \land Y \in V))$
37	36	ancrd	$⊢ φ \to (((X \subseteq A \land Y \subseteq B) \land R [X] = Y) \to ((X \in V \land Y \in V) \land ((X \subseteq A \land Y \subseteq B) \land R [X] = Y)))$
38	26 37	impbid2	$⊢ φ \to (((X \in V \land Y \in V) \land ((X \subseteq A \land Y \subseteq B) \land R [X] = Y)) \leftrightarrow ((X \subseteq A \land Y \subseteq B) \land R [X] = Y))$
39	8 25 38	3bitrd	$⊢ φ \to (X (A 𝒫_{*} B) (R) Y \leftrightarrow ((X \subseteq A \land Y \subseteq B) \land R [X] = Y))$

Metamath Proof Explorer

Theorem bj-imdirval3

Proof