iblsplitf

Description: A version of iblsplit using bound-variable hypotheses instead of distinct variable conditions". (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	iblsplitf.X	$⊢ Ⅎ x φ$
	iblsplitf.vol	$⊢ φ \to {vol}^{*} (A \cap B) = 0$
	iblsplitf.u	$⊢ φ \to U = A \cup B$
	iblsplitf.c	$⊢ (φ \land x \in U) \to C \in ℂ$
	iblsplitf.a	$⊢ φ \to (x \in A ⟼ C) \in 𝐿^{1}$
	iblsplitf.b	$⊢ φ \to (x \in B ⟼ C) \in 𝐿^{1}$
Assertion	iblsplitf	$⊢ φ \to (x \in U ⟼ C) \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		iblsplitf.X	$⊢ Ⅎ x φ$
2		iblsplitf.vol	$⊢ φ \to {vol}^{*} (A \cap B) = 0$
3		iblsplitf.u	$⊢ φ \to U = A \cup B$
4		iblsplitf.c	$⊢ (φ \land x \in U) \to C \in ℂ$
5		iblsplitf.a	$⊢ φ \to (x \in A ⟼ C) \in 𝐿^{1}$
6		iblsplitf.b	$⊢ φ \to (x \in B ⟼ C) \in 𝐿^{1}$
7		nfcv	$⊢ \underline{Ⅎ} y C$
8		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ C$
9		csbeq1a	$⊢ x = y \to C = ⦋ y / x ⦌ C$
10	7 8 9	cbvmpt	$⊢ (x \in U ⟼ C) = (y \in U ⟼ ⦋ y / x ⦌ C)$
11		simpr	$⊢ (φ \land y \in U) \to y \in U$
12		nfv	$⊢ Ⅎ x y \in U$
13	1 12	nfan	$⊢ Ⅎ x (φ \land y \in U)$
14	4	adantlr	$⊢ ((φ \land y \in U) \land x \in U) \to C \in ℂ$
15	14	ex	$⊢ (φ \land y \in U) \to (x \in U \to C \in ℂ)$
16	13 15	ralrimi	$⊢ (φ \land y \in U) \to \forall x \in U C \in ℂ$
17		rspcsbela	$⊢ (y \in U \land \forall x \in U C \in ℂ) \to ⦋ y / x ⦌ C \in ℂ$
18	11 16 17	syl2anc	$⊢ (φ \land y \in U) \to ⦋ y / x ⦌ C \in ℂ$
19	9	equcoms	$⊢ y = x \to C = ⦋ y / x ⦌ C$
20	19	eqcomd	$⊢ y = x \to ⦋ y / x ⦌ C = C$
21	8 7 20	cbvmpt	$⊢ (y \in A ⟼ ⦋ y / x ⦌ C) = (x \in A ⟼ C)$
22	21 5	eqeltrid	$⊢ φ \to (y \in A ⟼ ⦋ y / x ⦌ C) \in 𝐿^{1}$
23	8 7 20	cbvmpt	$⊢ (y \in B ⟼ ⦋ y / x ⦌ C) = (x \in B ⟼ C)$
24	23 6	eqeltrid	$⊢ φ \to (y \in B ⟼ ⦋ y / x ⦌ C) \in 𝐿^{1}$
25	2 3 18 22 24	iblsplit	$⊢ φ \to (y \in U ⟼ ⦋ y / x ⦌ C) \in 𝐿^{1}$
26	10 25	eqeltrid	$⊢ φ \to (x \in U ⟼ C) \in 𝐿^{1}$

Metamath Proof Explorer

Theorem iblsplitf

Proof