pmtrdifellem3

	Ref	Expression
Hypotheses	pmtrdifel.t	$⊢ T = ran pmTrsp (N ∖ \{K\})$
	pmtrdifel.r	$⊢ R = ran pmTrsp (N)$
	pmtrdifel.0	$⊢ S = pmTrsp (N) (dom (Q ∖ I))$
Assertion	pmtrdifellem3	$⊢ Q \in T \to \forall x \in (N ∖ \{K\}) Q (x) = S (x)$

Proof

Step	Hyp	Ref	Expression
1		pmtrdifel.t	$⊢ T = ran pmTrsp (N ∖ \{K\})$
2		pmtrdifel.r	$⊢ R = ran pmTrsp (N)$
3		pmtrdifel.0	$⊢ S = pmTrsp (N) (dom (Q ∖ I))$
4	1 2 3	pmtrdifellem2	$⊢ Q \in T \to dom (S ∖ I) = dom (Q ∖ I)$
5	4	adantr	$⊢ (Q \in T \land x \in (N ∖ \{K\})) \to dom (S ∖ I) = dom (Q ∖ I)$
6	5	eleq2d	$⊢ (Q \in T \land x \in (N ∖ \{K\})) \to (x \in dom (S ∖ I) \leftrightarrow x \in dom (Q ∖ I))$
7	4	difeq1d	$⊢ Q \in T \to dom (S ∖ I) ∖ \{x\} = dom (Q ∖ I) ∖ \{x\}$
8	7	unieqd	$⊢ Q \in T \to ⋃ (dom (S ∖ I) ∖ \{x\}) = ⋃ (dom (Q ∖ I) ∖ \{x\})$
9	8	adantr	$⊢ (Q \in T \land x \in (N ∖ \{K\})) \to ⋃ (dom (S ∖ I) ∖ \{x\}) = ⋃ (dom (Q ∖ I) ∖ \{x\})$
10	6 9	ifbieq1d	$⊢ (Q \in T \land x \in (N ∖ \{K\})) \to if (x \in dom (S ∖ I), ⋃ (dom (S ∖ I) ∖ \{x\}), x) = if (x \in dom (Q ∖ I), ⋃ (dom (Q ∖ I) ∖ \{x\}), x)$
11	1 2 3	pmtrdifellem1	$⊢ Q \in T \to S \in R$
12		eldifi	$⊢ x \in (N ∖ \{K\}) \to x \in N$
13		eqid	$⊢ pmTrsp (N) = pmTrsp (N)$
14		eqid	$⊢ dom (S ∖ I) = dom (S ∖ I)$
15	13 2 14	pmtrffv	$⊢ (S \in R \land x \in N) \to S (x) = if (x \in dom (S ∖ I), ⋃ (dom (S ∖ I) ∖ \{x\}), x)$
16	11 12 15	syl2an	$⊢ (Q \in T \land x \in (N ∖ \{K\})) \to S (x) = if (x \in dom (S ∖ I), ⋃ (dom (S ∖ I) ∖ \{x\}), x)$
17		eqid	$⊢ pmTrsp (N ∖ \{K\}) = pmTrsp (N ∖ \{K\})$
18		eqid	$⊢ dom (Q ∖ I) = dom (Q ∖ I)$
19	17 1 18	pmtrffv	$⊢ (Q \in T \land x \in (N ∖ \{K\})) \to Q (x) = if (x \in dom (Q ∖ I), ⋃ (dom (Q ∖ I) ∖ \{x\}), x)$
20	10 16 19	3eqtr4rd	$⊢ (Q \in T \land x \in (N ∖ \{K\})) \to Q (x) = S (x)$
21	20	ralrimiva	$⊢ Q \in T \to \forall x \in (N ∖ \{K\}) Q (x) = S (x)$

Metamath Proof Explorer

Theorem pmtrdifellem3

Proof