cantnfrescl

Description: A function is finitely supported from B to A iff the extended function is finitely supported from D to A . (Contributed by Mario Carneiro, 25-May-2015)

	Ref	Expression
Hypotheses	cantnfs.s	$⊢ S = dom (A CNF B)$
	cantnfs.a	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	cantnfrescl.d	$⊢ φ \to D \in On$
	cantnfrescl.b	$⊢ φ \to B \subseteq D$
	cantnfrescl.x	$⊢ (φ \land n \in (D ∖ B)) \to X = \emptyset$
	cantnfrescl.a	$⊢ φ \to \emptyset \in A$
	cantnfrescl.t	$⊢ T = dom (A CNF D)$
Assertion	cantnfrescl	$⊢ φ \to ((n \in B ⟼ X) \in S \leftrightarrow (n \in D ⟼ X) \in T)$

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	$⊢ S = dom (A CNF B)$
2		cantnfs.a	$⊢ φ \to A \in On$
3		cantnfs.b	$⊢ φ \to B \in On$
4		cantnfrescl.d	$⊢ φ \to D \in On$
5		cantnfrescl.b	$⊢ φ \to B \subseteq D$
6		cantnfrescl.x	$⊢ (φ \land n \in (D ∖ B)) \to X = \emptyset$
7		cantnfrescl.a	$⊢ φ \to \emptyset \in A$
8		cantnfrescl.t	$⊢ T = dom (A CNF D)$
9	7	adantr	$⊢ (φ \land n \in (D ∖ B)) \to \emptyset \in A$
10	6 9	eqeltrd	$⊢ (φ \land n \in (D ∖ B)) \to X \in A$
11	10	ralrimiva	$⊢ φ \to \forall n \in (D ∖ B) X \in A$
12	5 11	raldifeq	$⊢ φ \to (\forall n \in B X \in A \leftrightarrow \forall n \in D X \in A)$
13		eqid	$⊢ (n \in B ⟼ X) = (n \in B ⟼ X)$
14	13	fmpt	$⊢ \forall n \in B X \in A \leftrightarrow (n \in B ⟼ X) : B ⟶ A$
15		eqid	$⊢ (n \in D ⟼ X) = (n \in D ⟼ X)$
16	15	fmpt	$⊢ \forall n \in D X \in A \leftrightarrow (n \in D ⟼ X) : D ⟶ A$
17	12 14 16	3bitr3g	$⊢ φ \to ((n \in B ⟼ X) : B ⟶ A \leftrightarrow (n \in D ⟼ X) : D ⟶ A)$
18	3	mptexd	$⊢ φ \to (n \in B ⟼ X) \in V$
19		funmpt	$⊢ Fun (n \in B ⟼ X)$
20	19	a1i	$⊢ φ \to Fun (n \in B ⟼ X)$
21	4	mptexd	$⊢ φ \to (n \in D ⟼ X) \in V$
22		funmpt	$⊢ Fun (n \in D ⟼ X)$
23	21 22	jctir	$⊢ φ \to ((n \in D ⟼ X) \in V \land Fun (n \in D ⟼ X))$
24	18 20 23	jca31	$⊢ φ \to (((n \in B ⟼ X) \in V \land Fun (n \in B ⟼ X)) \land ((n \in D ⟼ X) \in V \land Fun (n \in D ⟼ X)))$
25	4 5 6	extmptsuppeq	$⊢ φ \to (n \in B ⟼ X) supp \emptyset = (n \in D ⟼ X) supp \emptyset$
26		suppeqfsuppbi	$⊢ (((n \in B ⟼ X) \in V \land Fun (n \in B ⟼ X)) \land ((n \in D ⟼ X) \in V \land Fun (n \in D ⟼ X))) \to ((n \in B ⟼ X) supp \emptyset = (n \in D ⟼ X) supp \emptyset \to ({finSupp}_{\emptyset} ((n \in B ⟼ X)) \leftrightarrow {finSupp}_{\emptyset} ((n \in D ⟼ X))))$
27	24 25 26	sylc	$⊢ φ \to ({finSupp}_{\emptyset} ((n \in B ⟼ X)) \leftrightarrow {finSupp}_{\emptyset} ((n \in D ⟼ X)))$
28	17 27	anbi12d	$⊢ φ \to (((n \in B ⟼ X) : B ⟶ A \land {finSupp}_{\emptyset} ((n \in B ⟼ X))) \leftrightarrow ((n \in D ⟼ X) : D ⟶ A \land {finSupp}_{\emptyset} ((n \in D ⟼ X))))$
29	1 2 3	cantnfs	$⊢ φ \to ((n \in B ⟼ X) \in S \leftrightarrow ((n \in B ⟼ X) : B ⟶ A \land {finSupp}_{\emptyset} ((n \in B ⟼ X))))$
30	8 2 4	cantnfs	$⊢ φ \to ((n \in D ⟼ X) \in T \leftrightarrow ((n \in D ⟼ X) : D ⟶ A \land {finSupp}_{\emptyset} ((n \in D ⟼ X))))$
31	28 29 30	3bitr4d	$⊢ φ \to ((n \in B ⟼ X) \in S \leftrightarrow (n \in D ⟼ X) \in T)$

Metamath Proof Explorer

Theorem cantnfrescl

Proof