axprlem4

Description: Lemma for axpr . The first 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	axprlem4	$⊢ (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = x) \to \exists s (s \in p \land if- (\exists n n \in s, w = x, w = y))$

Proof

Step	Hyp	Ref	Expression
1		axprlem1	$⊢ \exists s \forall n (\forall t \neg t \in n \to n \in s)$
2	1	bm1.3ii	$⊢ \exists s \forall n (n \in s \leftrightarrow \forall t \neg t \in n)$
3		nfa1	$⊢ Ⅎ s \forall s (\forall n \in s \forall t \neg t \in n \to s \in p)$
4		nfv	$⊢ Ⅎ s w = x$
5	3 4	nfan	$⊢ Ⅎ s (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = x)$
6		biimp	$⊢ (n \in s \leftrightarrow \forall t \neg t \in n) \to (n \in s \to \forall t \neg t \in n)$
7	6	alimi	$⊢ \forall n (n \in s \leftrightarrow \forall t \neg t \in n) \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 (n \in s \leftrightarrow \forall t \neg t \in n) \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	9 10	mpan9	$⊢ (\forall n (n \in s \leftrightarrow \forall t \neg t \in n) \land \forall s (\forall n \in s \forall t \neg t \in n \to s \in p)) \to s \in p$
12	11	adantrr	$⊢ (\forall n (n \in s \leftrightarrow \forall t \neg t \in n) \land (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = x)) \to s \in p$
13		ax-nul	$⊢ \exists n \forall t \neg t \in n$
14		nfa1	$⊢ Ⅎ n \forall n (n \in s \leftrightarrow \forall t \neg t \in n)$
15		sp	$⊢ \forall n (n \in s \leftrightarrow \forall t \neg t \in n) \to (n \in s \leftrightarrow \forall t \neg t \in n)$
16	15	biimprd	$⊢ \forall n (n \in s \leftrightarrow \forall t \neg t \in n) \to (\forall t \neg t \in n \to n \in s)$
17	14 16	eximd	$⊢ \forall n (n \in s \leftrightarrow \forall t \neg t \in n) \to (\exists n \forall t \neg t \in n \to \exists n n \in s)$
18	13 17	mpi	$⊢ \forall n (n \in s \leftrightarrow \forall t \neg t \in n) \to \exists n n \in s$
19		simprr	$⊢ (\forall n (n \in s \leftrightarrow \forall t \neg t \in n) \land (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = x)) \to w = x$
20		ifptru	$⊢ \exists n n \in s \to (if- (\exists n n \in s, w = x, w = y) \leftrightarrow w = x)$
21	20	biimpar	$⊢ (\exists n n \in s \land w = x) \to if- (\exists n n \in s, w = x, w = y)$
22	18 19 21	syl2an2r	$⊢ (\forall n (n \in s \leftrightarrow \forall t \neg t \in n) \land (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = x)) \to if- (\exists n n \in s, w = x, w = y)$
23	12 22	jca	$⊢ (\forall n (n \in s \leftrightarrow \forall t \neg t \in n) \land (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = x)) \to (s \in p \land if- (\exists n n \in s, w = x, w = y))$
24	23	expcom	$⊢ (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = x) \to (\forall n (n \in s \leftrightarrow \forall t \neg t \in n) \to (s \in p \land if- (\exists n n \in s, w = x, w = y)))$
25	5 24	eximd	$⊢ (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = x) \to (\exists s \forall n (n \in s \leftrightarrow \forall t \neg t \in n) \to \exists s (s \in p \land if- (\exists n n \in s, w = x, w = y)))$
26	2 25	mpi	$⊢ (\forall s (\forall n \in s \forall t \neg t \in n \to s \in p) \land w = x) \to \exists s (s \in p \land if- (\exists n n \in s, w = x, w = y))$

Metamath Proof Explorer

Theorem axprlem4

Proof