intabs

Description: Absorption of a redundant conjunct in the intersection of a class abstraction. (Contributed by NM, 3-Jul-2005)

	Ref	Expression
Hypotheses	intabs.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	intabs.2	$⊢ x = ⋂ \{y \| ψ\} \to (φ \leftrightarrow χ)$
	intabs.3	$⊢ (⋂ \{y \| ψ\} \subseteq A \land χ)$
Assertion	intabs	$⊢ ⋂ \{x \| (x \subseteq A \land φ)\} = ⋂ \{x \| φ\}$

Proof

Step	Hyp	Ref	Expression
1		intabs.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		intabs.2	$⊢ x = ⋂ \{y \| ψ\} \to (φ \leftrightarrow χ)$
3		intabs.3	$⊢ (⋂ \{y \| ψ\} \subseteq A \land χ)$
4		sseq1	$⊢ x = ⋂ \{y \| ψ\} \to (x \subseteq A \leftrightarrow ⋂ \{y \| ψ\} \subseteq A)$
5	4 2	anbi12d	$⊢ x = ⋂ \{y \| ψ\} \to ((x \subseteq A \land φ) \leftrightarrow (⋂ \{y \| ψ\} \subseteq A \land χ))$
6	5 3	intmin3	$⊢ ⋂ \{y \| ψ\} \in V \to ⋂ \{x \| (x \subseteq A \land φ)\} \subseteq ⋂ \{y \| ψ\}$
7		intnex	$⊢ \neg ⋂ \{y \| ψ\} \in V \leftrightarrow ⋂ \{y \| ψ\} = V$
8		ssv	$⊢ ⋂ \{x \| (x \subseteq A \land φ)\} \subseteq V$
9		sseq2	$⊢ ⋂ \{y \| ψ\} = V \to (⋂ \{x \| (x \subseteq A \land φ)\} \subseteq ⋂ \{y \| ψ\} \leftrightarrow ⋂ \{x \| (x \subseteq A \land φ)\} \subseteq V)$
10	8 9	mpbiri	$⊢ ⋂ \{y \| ψ\} = V \to ⋂ \{x \| (x \subseteq A \land φ)\} \subseteq ⋂ \{y \| ψ\}$
11	7 10	sylbi	$⊢ \neg ⋂ \{y \| ψ\} \in V \to ⋂ \{x \| (x \subseteq A \land φ)\} \subseteq ⋂ \{y \| ψ\}$
12	6 11	pm2.61i	$⊢ ⋂ \{x \| (x \subseteq A \land φ)\} \subseteq ⋂ \{y \| ψ\}$
13	1	cbvabv	$⊢ \{x \| φ\} = \{y \| ψ\}$
14	13	inteqi	$⊢ ⋂ \{x \| φ\} = ⋂ \{y \| ψ\}$
15	12 14	sseqtrri	$⊢ ⋂ \{x \| (x \subseteq A \land φ)\} \subseteq ⋂ \{x \| φ\}$
16		simpr	$⊢ (x \subseteq A \land φ) \to φ$
17	16	ss2abi	$⊢ \{x \| (x \subseteq A \land φ)\} \subseteq \{x \| φ\}$
18		intss	$⊢ \{x \| (x \subseteq A \land φ)\} \subseteq \{x \| φ\} \to ⋂ \{x \| φ\} \subseteq ⋂ \{x \| (x \subseteq A \land φ)\}$
19	17 18	ax-mp	$⊢ ⋂ \{x \| φ\} \subseteq ⋂ \{x \| (x \subseteq A \land φ)\}$
20	15 19	eqssi	$⊢ ⋂ \{x \| (x \subseteq A \land φ)\} = ⋂ \{x \| φ\}$

Metamath Proof Explorer

Theorem intabs

Proof