elovmpt3rab1

Description: Implications for the value of an operation defined by the maps-to notation with a function into a class abstraction as a result having an element. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018) (Revised by AV, 16-May-2019)

	Ref	Expression
Hypotheses	ovmpt3rab1.o	$⊢ O = (x \in V, y \in V ⟼ (z \in M ⟼ \{a \in N \| φ\}))$
	ovmpt3rab1.m	$⊢ (x = X \land y = Y) \to M = K$
	ovmpt3rab1.n	$⊢ (x = X \land y = Y) \to N = L$
Assertion	elovmpt3rab1	$⊢ (K \in U \land L \in T) \to (A \in (X O Y) (Z) \to ((X \in V \land Y \in V) \land (Z \in K \land A \in L)))$

Proof

Step	Hyp	Ref	Expression
1		ovmpt3rab1.o	$⊢ O = (x \in V, y \in V ⟼ (z \in M ⟼ \{a \in N \| φ\}))$
2		ovmpt3rab1.m	$⊢ (x = X \land y = Y) \to M = K$
3		ovmpt3rab1.n	$⊢ (x = X \land y = Y) \to N = L$
4	1	elovmpt3imp	$⊢ A \in (X O Y) (Z) \to (X \in V \land Y \in V)$
5		simprl	$⊢ (A \in (X O Y) (Z) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T))) \to (X \in V \land Y \in V)$
6		elfvdm	$⊢ A \in (X O Y) (Z) \to Z \in dom (X O Y)$
7		simpl	$⊢ (X \in V \land Y \in V) \to X \in V$
8	7	adantr	$⊢ ((X \in V \land Y \in V) \land (K \in U \land L \in T)) \to X \in V$
9		simplr	$⊢ ((X \in V \land Y \in V) \land (K \in U \land L \in T)) \to Y \in V$
10		simprl	$⊢ ((X \in V \land Y \in V) \land (K \in U \land L \in T)) \to K \in U$
11		simprr	$⊢ ((X \in V \land Y \in V) \land (K \in U \land L \in T)) \to L \in T$
12	1 2 3	ovmpt3rabdm	$⊢ ((X \in V \land Y \in V \land K \in U) \land L \in T) \to dom (X O Y) = K$
13	8 9 10 11 12	syl31anc	$⊢ ((X \in V \land Y \in V) \land (K \in U \land L \in T)) \to dom (X O Y) = K$
14	13	eleq2d	$⊢ ((X \in V \land Y \in V) \land (K \in U \land L \in T)) \to (Z \in dom (X O Y) \leftrightarrow Z \in K)$
15	14	biimpcd	$⊢ Z \in dom (X O Y) \to (((X \in V \land Y \in V) \land (K \in U \land L \in T)) \to Z \in K)$
16	15	adantr	$⊢ (Z \in dom (X O Y) \land A \in (X O Y) (Z)) \to (((X \in V \land Y \in V) \land (K \in U \land L \in T)) \to Z \in K)$
17	16	imp	$⊢ ((Z \in dom (X O Y) \land A \in (X O Y) (Z)) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T))) \to Z \in K$
18		simpl	$⊢ (Z \in K \land ((Z \in dom (X O Y) \land A \in (X O Y) (Z)) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T)))) \to Z \in K$
19		simplr	$⊢ ((Z \in dom (X O Y) \land A \in (X O Y) (Z)) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T))) \to A \in (X O Y) (Z)$
20	19	adantl	$⊢ (Z \in K \land ((Z \in dom (X O Y) \land A \in (X O Y) (Z)) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T)))) \to A \in (X O Y) (Z)$
21		simpl	$⊢ (K \in U \land L \in T) \to K \in U$
22	21	anim2i	$⊢ ((X \in V \land Y \in V) \land (K \in U \land L \in T)) \to ((X \in V \land Y \in V) \land K \in U)$
23		df-3an	$⊢ (X \in V \land Y \in V \land K \in U) \leftrightarrow ((X \in V \land Y \in V) \land K \in U)$
24	22 23	sylibr	$⊢ ((X \in V \land Y \in V) \land (K \in U \land L \in T)) \to (X \in V \land Y \in V \land K \in U)$
25	24	ad2antll	$⊢ (Z \in K \land ((Z \in dom (X O Y) \land A \in (X O Y) (Z)) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T)))) \to (X \in V \land Y \in V \land K \in U)$
26		sbceq1a	$⊢ y = Y \to (φ \leftrightarrow \underset{˙}{[} Y / y \underset{˙}{]} φ)$
27		sbceq1a	$⊢ x = X \to (\underset{˙}{[} Y / y \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ)$
28	26 27	sylan9bbr	$⊢ (x = X \land y = Y) \to (φ \leftrightarrow \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ)$
29		nfsbc1v	$⊢ Ⅎ x \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ$
30		nfcv	$⊢ \underline{Ⅎ} y X$
31		nfsbc1v	$⊢ Ⅎ y \underset{˙}{[} Y / y \underset{˙}{]} φ$
32	30 31	nfsbcw	$⊢ Ⅎ y \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ$
33	1 2 3 28 29 32	ovmpt3rab1	$⊢ (X \in V \land Y \in V \land K \in U) \to X O Y = (z \in K ⟼ \{a \in L \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\})$
34	33	fveq1d	$⊢ (X \in V \land Y \in V \land K \in U) \to (X O Y) (Z) = (z \in K ⟼ \{a \in L \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}) (Z)$
35	25 34	syl	$⊢ (Z \in K \land ((Z \in dom (X O Y) \land A \in (X O Y) (Z)) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T)))) \to (X O Y) (Z) = (z \in K ⟼ \{a \in L \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}) (Z)$
36		rabexg	$⊢ L \in T \to \{a \in L \| \underset{˙}{[} Z / z \underset{˙}{]} \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\} \in V$
37	36	adantl	$⊢ (K \in U \land L \in T) \to \{a \in L \| \underset{˙}{[} Z / z \underset{˙}{]} \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\} \in V$
38	37	ad2antll	$⊢ ((Z \in dom (X O Y) \land A \in (X O Y) (Z)) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T))) \to \{a \in L \| \underset{˙}{[} Z / z \underset{˙}{]} \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\} \in V$
39		nfcv	$⊢ \underline{Ⅎ} z Z$
40		nfsbc1v	$⊢ Ⅎ z \underset{˙}{[} Z / z \underset{˙}{]} \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ$
41		nfcv	$⊢ \underline{Ⅎ} z L$
42	40 41	nfrabw	$⊢ \underline{Ⅎ} z \{a \in L \| \underset{˙}{[} Z / z \underset{˙}{]} \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}$
43		sbceq1a	$⊢ z = Z \to (\underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} Z / z \underset{˙}{]} \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ)$
44	43	rabbidv	$⊢ z = Z \to \{a \in L \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\} = \{a \in L \| \underset{˙}{[} Z / z \underset{˙}{]} \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}$
45		eqid	$⊢ (z \in K ⟼ \{a \in L \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}) = (z \in K ⟼ \{a \in L \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\})$
46	39 42 44 45	fvmptf	$⊢ (Z \in K \land \{a \in L \| \underset{˙}{[} Z / z \underset{˙}{]} \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\} \in V) \to (z \in K ⟼ \{a \in L \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}) (Z) = \{a \in L \| \underset{˙}{[} Z / z \underset{˙}{]} \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}$
47	38 46	sylan2	$⊢ (Z \in K \land ((Z \in dom (X O Y) \land A \in (X O Y) (Z)) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T)))) \to (z \in K ⟼ \{a \in L \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}) (Z) = \{a \in L \| \underset{˙}{[} Z / z \underset{˙}{]} \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}$
48	35 47	eqtr2d	$⊢ (Z \in K \land ((Z \in dom (X O Y) \land A \in (X O Y) (Z)) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T)))) \to \{a \in L \| \underset{˙}{[} Z / z \underset{˙}{]} \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\} = (X O Y) (Z)$
49	20 48	eleqtrrd	$⊢ (Z \in K \land ((Z \in dom (X O Y) \land A \in (X O Y) (Z)) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T)))) \to A \in \{a \in L \| \underset{˙}{[} Z / z \underset{˙}{]} \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}$
50		elrabi	$⊢ A \in \{a \in L \| \underset{˙}{[} Z / z \underset{˙}{]} \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\} \to A \in L$
51	49 50	syl	$⊢ (Z \in K \land ((Z \in dom (X O Y) \land A \in (X O Y) (Z)) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T)))) \to A \in L$
52	18 51	jca	$⊢ (Z \in K \land ((Z \in dom (X O Y) \land A \in (X O Y) (Z)) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T)))) \to (Z \in K \land A \in L)$
53	17 52	mpancom	$⊢ ((Z \in dom (X O Y) \land A \in (X O Y) (Z)) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T))) \to (Z \in K \land A \in L)$
54	53	exp31	$⊢ Z \in dom (X O Y) \to (A \in (X O Y) (Z) \to (((X \in V \land Y \in V) \land (K \in U \land L \in T)) \to (Z \in K \land A \in L)))$
55	6 54	mpcom	$⊢ A \in (X O Y) (Z) \to (((X \in V \land Y \in V) \land (K \in U \land L \in T)) \to (Z \in K \land A \in L))$
56	55	imp	$⊢ (A \in (X O Y) (Z) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T))) \to (Z \in K \land A \in L)$
57	5 56	jca	$⊢ (A \in (X O Y) (Z) \land ((X \in V \land Y \in V) \land (K \in U \land L \in T))) \to ((X \in V \land Y \in V) \land (Z \in K \land A \in L))$
58	57	exp32	$⊢ A \in (X O Y) (Z) \to ((X \in V \land Y \in V) \to ((K \in U \land L \in T) \to ((X \in V \land Y \in V) \land (Z \in K \land A \in L))))$
59	4 58	mpd	$⊢ A \in (X O Y) (Z) \to ((K \in U \land L \in T) \to ((X \in V \land Y \in V) \land (Z \in K \land A \in L)))$
60	59	com12	$⊢ (K \in U \land L \in T) \to (A \in (X O Y) (Z) \to ((X \in V \land Y \in V) \land (Z \in K \land A \in L)))$

Metamath Proof Explorer

Theorem elovmpt3rab1

Proof