axprlem5

Description: Lemma for axpr . The second element of the pair is included in any superset of the set whose existence is asserted by the axiom of replacement. (Contributed by Rohan Ridenour, 10-Aug-2023) (Revised by BJ, 13-Aug-2023)

		Ref	Expression
	Assertion	axprlem5	$⊢ (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y) \to \exists s (s \in p \land if- (\exists n n \in s, w = x, w = y))$

Proof

Step	Hyp	Ref	Expression
1		ax-nul	$⊢ \exists s \forall n \neg n \in s$
2		nfa1	$⊢ Ⅎ s \forall s (\forall n \in s \forall t \neg t \in n \to s \in p)$
3		nfv	$⊢ Ⅎ s w = y$
4	2 3	nfan	$⊢ Ⅎ s (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y)$
5		pm2.21	$⊢ \neg n \in s \to (n \in s \to \forall t \neg t \in n)$
6	5	alimi	$⊢ \forall n \neg n \in s \to \forall n (n \in s \to \forall t \neg t \in n)$
7	6	adantr	$⊢ (\forall n \neg n \in s \land (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y)) \to \forall n (n \in s \to \forall t \neg t \in n)$
8		df-ral	$⊢ \forall n \in s \forall t \neg t \in n \leftrightarrow \forall n (n \in s \to \forall t \neg t \in n)$
9	7 8	sylibr	$⊢ (\forall n \neg n \in s \land (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y)) \to \forall n \in s \forall t \neg t \in n$
10		sp	$⊢ \forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \to (\forall n \in s \forall t \neg t \in n \to s \in p)$
11	10	ad2antrl	$⊢ (\forall n \neg n \in s \land (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y)) \to (\forall n \in s \forall t \neg t \in n \to s \in p)$
12	9 11	mpd	$⊢ (\forall n \neg n \in s \land (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y)) \to s \in p$
13		simpl	$⊢ (\forall n \neg n \in s \land (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y)) \to \forall n \neg n \in s$
14		alnex	$⊢ \forall n \neg n \in s \leftrightarrow \neg \exists n n \in s$
15	13 14	sylib	$⊢ (\forall n \neg n \in s \land (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y)) \to \neg \exists n n \in s$
16		simprr	$⊢ (\forall n \neg n \in s \land (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y)) \to w = y$
17		ifpfal	$⊢ \neg \exists n n \in s \to (if- (\exists n n \in s, w = x, w = y) \leftrightarrow w = y)$
18	17	biimpar	$⊢ (\neg \exists n n \in s \land w = y) \to if- (\exists n n \in s, w = x, w = y)$
19	15 16 18	syl2anc	$⊢ (\forall n \neg n \in s \land (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y)) \to if- (\exists n n \in s, w = x, w = y)$
20	12 19	jca	$⊢ (\forall n \neg n \in s \land (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y)) \to (s \in p \land if- (\exists n n \in s, w = x, w = y))$
21	20	expcom	$⊢ (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y) \to (\forall n \neg n \in s \to (s \in p \land if- (\exists n n \in s, w = x, w = y)))$
22	4 21	eximd	$⊢ (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y) \to (\exists s \forall n \neg n \in s \to \exists s (s \in p \land if- (\exists n n \in s, w = x, w = y)))$
23	1 22	mpi	$⊢ (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = y) \to \exists s (s \in p \land if- (\exists n n \in s, w = x, w = y))$

Metamath Proof Explorer

Theorem axprlem5

Proof