pgindnf

Description: Version of pgind with extraneous not-free requirements. (Contributed by Emmett Weisz, 27-May-2024) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pgindnf.1	$⊢ Ⅎ x φ$
	pgindnf.2	$⊢ Ⅎ y φ$
	pgindnf.3	$⊢ x = y \to (ψ \leftrightarrow χ)$
	pgindnf.4	$⊢ y = A \to (χ \leftrightarrow θ)$
	pgindnf.5	$⊢ φ \to \forall x (\forall y \in (1^{st} (x) \cup 2^{nd} (x)) χ \to ψ)$
Assertion	pgindnf	$⊢ φ \to (A \in Pg \to θ)$

Proof

Step	Hyp	Ref	Expression
1		pgindnf.1	$⊢ Ⅎ x φ$
2		pgindnf.2	$⊢ Ⅎ y φ$
3		pgindnf.3	$⊢ x = y \to (ψ \leftrightarrow χ)$
4		pgindnf.4	$⊢ y = A \to (χ \leftrightarrow θ)$
5		pgindnf.5	$⊢ φ \to \forall x (\forall y \in (1^{st} (x) \cup 2^{nd} (x)) χ \to ψ)$
6		df-pg	$⊢ Pg = setrecs ((a \in V ⟼ 𝒫 a \times 𝒫 a))$
7		nfv	$⊢ Ⅎ x \forall y \in z χ$
8	1 7	nfan	$⊢ Ⅎ x (φ \land \forall y \in z χ)$
9		pgindlem	$⊢ x \in (𝒫 z \times 𝒫 z) \to 1^{st} (x) \cup 2^{nd} (x) \subseteq z$
10	9	sseld	$⊢ x \in (𝒫 z \times 𝒫 z) \to (y \in (1^{st} (x) \cup 2^{nd} (x)) \to y \in z)$
11	10	imim1d	$⊢ x \in (𝒫 z \times 𝒫 z) \to ((y \in z \to χ) \to (y \in (1^{st} (x) \cup 2^{nd} (x)) \to χ))$
12	11	ralimdv2	$⊢ x \in (𝒫 z \times 𝒫 z) \to (\forall y \in z χ \to \forall y \in (1^{st} (x) \cup 2^{nd} (x)) χ)$
13	5	19.21bi	$⊢ φ \to (\forall y \in (1^{st} (x) \cup 2^{nd} (x)) χ \to ψ)$
14	12 13	sylan9r	$⊢ (φ \land x \in (𝒫 z \times 𝒫 z)) \to (\forall y \in z χ \to ψ)$
15	14	impancom	$⊢ (φ \land \forall y \in z χ) \to (x \in (𝒫 z \times 𝒫 z) \to ψ)$
16	8 15	ralrimi	$⊢ (φ \land \forall y \in z χ) \to \forall x \in (𝒫 z \times 𝒫 z) ψ$
17		vex	$⊢ z \in V$
18		pweq	$⊢ a = z \to 𝒫 a = 𝒫 z$
19	18	sqxpeqd	$⊢ a = z \to 𝒫 a \times 𝒫 a = 𝒫 z \times 𝒫 z$
20		eqid	$⊢ (a \in V ⟼ 𝒫 a \times 𝒫 a) = (a \in V ⟼ 𝒫 a \times 𝒫 a)$
21		vpwex	$⊢ 𝒫 z \in V$
22	21 21	xpex	$⊢ 𝒫 z \times 𝒫 z \in V$
23	19 20 22	fvmpt	$⊢ z \in V \to (a \in V ⟼ 𝒫 a \times 𝒫 a) (z) = 𝒫 z \times 𝒫 z$
24	17 23	ax-mp	$⊢ (a \in V ⟼ 𝒫 a \times 𝒫 a) (z) = 𝒫 z \times 𝒫 z$
25	24	eqcomi	$⊢ 𝒫 z \times 𝒫 z = (a \in V ⟼ 𝒫 a \times 𝒫 a) (z)$
26	25	a1i	$⊢ x = y \to 𝒫 z \times 𝒫 z = (a \in V ⟼ 𝒫 a \times 𝒫 a) (z)$
27	3 26	cbvralv2	$⊢ \forall x \in (𝒫 z \times 𝒫 z) ψ \leftrightarrow \forall y \in (a \in V ⟼ 𝒫 a \times 𝒫 a) (z) χ$
28	16 27	sylib	$⊢ (φ \land \forall y \in z χ) \to \forall y \in (a \in V ⟼ 𝒫 a \times 𝒫 a) (z) χ$
29	28	ex	$⊢ φ \to (\forall y \in z χ \to \forall y \in (a \in V ⟼ 𝒫 a \times 𝒫 a) (z) χ)$
30	29	alrimiv	$⊢ φ \to \forall z (\forall y \in z χ \to \forall y \in (a \in V ⟼ 𝒫 a \times 𝒫 a) (z) χ)$
31	6 4 30	setis	$⊢ φ \to (A \in Pg \to θ)$

Metamath Proof Explorer

Theorem pgindnf

Proof