weiunfr

Description: A well-founded relation on an indexed union can be constructed from a well-ordering on its index set and a collection of well-founded relations on its members. (Contributed by Matthew House, 23-Aug-2025)

	Ref	Expression
Hypotheses	weiunfr.1	$⊢ F = (w \in ⋃_{x \in A} B ⟼ (ι u \in \{x \in A \| w \in B\} \| \forall v \in \{x \in A \| w \in B\} \neg v R u))$
	weiunfr.2	$⊢ T = \{⟨y, z⟩ \| ((y \in ⋃_{x \in A} B \land z \in ⋃_{x \in A} B) \land (F (y) R F (z) \lor (F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z)))\}$
Assertion	weiunfr	$⊢ (R We A \land R Se A \land \forall x \in A S Fr B) \to T Fr ⋃_{x \in A} B$

Proof

Step	Hyp	Ref	Expression
1		weiunfr.1	$⊢ F = (w \in ⋃_{x \in A} B ⟼ (ι u \in \{x \in A \| w \in B\} \| \forall v \in \{x \in A \| w \in B\} \neg v R u))$
2		weiunfr.2	$⊢ T = \{⟨y, z⟩ \| ((y \in ⋃_{x \in A} B \land z \in ⋃_{x \in A} B) \land (F (y) R F (z) \lor (F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z)))\}$
3		breq2	$⊢ u = m \to (v R u \leftrightarrow v R m)$
4	3	notbid	$⊢ u = m \to (\neg v R u \leftrightarrow \neg v R m)$
5	4	ralbidv	$⊢ u = m \to (\forall v \in \{x \in A \| w \in B\} \neg v R u \leftrightarrow \forall v \in \{x \in A \| w \in B\} \neg v R m)$
6	5	cbvriotavw	$⊢ (ι u \in \{x \in A \| w \in B\} \| \forall v \in \{x \in A \| w \in B\} \neg v R u) = (ι m \in \{x \in A \| w \in B\} \| \forall v \in \{x \in A \| w \in B\} \neg v R m)$
7		nfcv	$⊢ \underline{Ⅎ} x A$
8		nfcv	$⊢ \underline{Ⅎ} l A$
9		nfv	$⊢ Ⅎ l w \in B$
10		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ l / x ⦌ B$
11	10	nfcri	$⊢ Ⅎ x w \in ⦋ l / x ⦌ B$
12		csbeq1a	$⊢ x = l \to B = ⦋ l / x ⦌ B$
13	12	eleq2d	$⊢ x = l \to (w \in B \leftrightarrow w \in ⦋ l / x ⦌ B)$
14	7 8 9 11 13	cbvrabw	$⊢ \{x \in A \| w \in B\} = \{l \in A \| w \in ⦋ l / x ⦌ B\}$
15		eleq1w	$⊢ w = k \to (w \in ⦋ l / x ⦌ B \leftrightarrow k \in ⦋ l / x ⦌ B)$
16	15	rabbidv	$⊢ w = k \to \{l \in A \| w \in ⦋ l / x ⦌ B\} = \{l \in A \| k \in ⦋ l / x ⦌ B\}$
17	14 16	eqtrid	$⊢ w = k \to \{x \in A \| w \in B\} = \{l \in A \| k \in ⦋ l / x ⦌ B\}$
18		breq1	$⊢ v = n \to (v R m \leftrightarrow n R m)$
19	18	notbid	$⊢ v = n \to (\neg v R m \leftrightarrow \neg n R m)$
20	19	adantl	$⊢ (w = k \land v = n) \to (\neg v R m \leftrightarrow \neg n R m)$
21	17	adantr	$⊢ (w = k \land v = n) \to \{x \in A \| w \in B\} = \{l \in A \| k \in ⦋ l / x ⦌ B\}$
22	20 21	cbvraldva2	$⊢ w = k \to (\forall v \in \{x \in A \| w \in B\} \neg v R m \leftrightarrow \forall n \in \{l \in A \| k \in ⦋ l / x ⦌ B\} \neg n R m)$
23	17 22	riotaeqbidv	$⊢ w = k \to (ι m \in \{x \in A \| w \in B\} \| \forall v \in \{x \in A \| w \in B\} \neg v R m) = (ι m \in \{l \in A \| k \in ⦋ l / x ⦌ B\} \| \forall n \in \{l \in A \| k \in ⦋ l / x ⦌ B\} \neg n R m)$
24	6 23	eqtrid	$⊢ w = k \to (ι u \in \{x \in A \| w \in B\} \| \forall v \in \{x \in A \| w \in B\} \neg v R u) = (ι m \in \{l \in A \| k \in ⦋ l / x ⦌ B\} \| \forall n \in \{l \in A \| k \in ⦋ l / x ⦌ B\} \neg n R m)$
25	24	cbvmptv	$⊢ (w \in ⋃_{x \in A} B ⟼ (ι u \in \{x \in A \| w \in B\} \| \forall v \in \{x \in A \| w \in B\} \neg v R u)) = (k \in ⋃_{x \in A} B ⟼ (ι m \in \{l \in A \| k \in ⦋ l / x ⦌ B\} \| \forall n \in \{l \in A \| k \in ⦋ l / x ⦌ B\} \neg n R m))$
26		nfcv	$⊢ \underline{Ⅎ} l B$
27	26 10 12	cbviun	$⊢ ⋃_{x \in A} B = ⋃_{l \in A} ⦋ l / x ⦌ B$
28	27	mpteq1i	$⊢ (k \in ⋃_{x \in A} B ⟼ (ι m \in \{l \in A \| k \in ⦋ l / x ⦌ B\} \| \forall n \in \{l \in A \| k \in ⦋ l / x ⦌ B\} \neg n R m)) = (k \in ⋃_{l \in A} ⦋ l / x ⦌ B ⟼ (ι m \in \{l \in A \| k \in ⦋ l / x ⦌ B\} \| \forall n \in \{l \in A \| k \in ⦋ l / x ⦌ B\} \neg n R m))$
29	1 25 28	3eqtri	$⊢ F = (k \in ⋃_{l \in A} ⦋ l / x ⦌ B ⟼ (ι m \in \{l \in A \| k \in ⦋ l / x ⦌ B\} \| \forall n \in \{l \in A \| k \in ⦋ l / x ⦌ B\} \neg n R m))$
30		simpl	$⊢ (y = o \land z = p) \to y = o$
31	27	a1i	$⊢ (y = o \land z = p) \to ⋃_{x \in A} B = ⋃_{l \in A} ⦋ l / x ⦌ B$
32	30 31	eleq12d	$⊢ (y = o \land z = p) \to (y \in ⋃_{x \in A} B \leftrightarrow o \in ⋃_{l \in A} ⦋ l / x ⦌ B)$
33		simpr	$⊢ (y = o \land z = p) \to z = p$
34	33 31	eleq12d	$⊢ (y = o \land z = p) \to (z \in ⋃_{x \in A} B \leftrightarrow p \in ⋃_{l \in A} ⦋ l / x ⦌ B)$
35	32 34	anbi12d	$⊢ (y = o \land z = p) \to ((y \in ⋃_{x \in A} B \land z \in ⋃_{x \in A} B) \leftrightarrow (o \in ⋃_{l \in A} ⦋ l / x ⦌ B \land p \in ⋃_{l \in A} ⦋ l / x ⦌ B))$
36	30	fveq2d	$⊢ (y = o \land z = p) \to F (y) = F (o)$
37	33	fveq2d	$⊢ (y = o \land z = p) \to F (z) = F (p)$
38	36 37	breq12d	$⊢ (y = o \land z = p) \to (F (y) R F (z) \leftrightarrow F (o) R F (p))$
39	36 37	eqeq12d	$⊢ (y = o \land z = p) \to (F (y) = F (z) \leftrightarrow F (o) = F (p))$
40	36	csbeq1d	$⊢ (y = o \land z = p) \to ⦋ F (y) / x ⦌ S = ⦋ F (o) / x ⦌ S$
41		csbcow	$⊢ ⦋ F (o) / l ⦌ ⦋ l / x ⦌ S = ⦋ F (o) / x ⦌ S$
42	40 41	eqtr4di	$⊢ (y = o \land z = p) \to ⦋ F (y) / x ⦌ S = ⦋ F (o) / l ⦌ ⦋ l / x ⦌ S$
43	30 42 33	breq123d	$⊢ (y = o \land z = p) \to (y ⦋ F (y) / x ⦌ S z \leftrightarrow o ⦋ F (o) / l ⦌ ⦋ l / x ⦌ S p)$
44	39 43	anbi12d	$⊢ (y = o \land z = p) \to ((F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z) \leftrightarrow (F (o) = F (p) \land o ⦋ F (o) / l ⦌ ⦋ l / x ⦌ S p))$
45	38 44	orbi12d	$⊢ (y = o \land z = p) \to ((F (y) R F (z) \lor (F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z)) \leftrightarrow (F (o) R F (p) \lor (F (o) = F (p) \land o ⦋ F (o) / l ⦌ ⦋ l / x ⦌ S p)))$
46	35 45	anbi12d	$⊢ (y = o \land z = p) \to (((y \in ⋃_{x \in A} B \land z \in ⋃_{x \in A} B) \land (F (y) R F (z) \lor (F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z))) \leftrightarrow ((o \in ⋃_{l \in A} ⦋ l / x ⦌ B \land p \in ⋃_{l \in A} ⦋ l / x ⦌ B) \land (F (o) R F (p) \lor (F (o) = F (p) \land o ⦋ F (o) / l ⦌ ⦋ l / x ⦌ S p))))$
47	46	cbvopabv	$⊢ \{⟨y, z⟩ \| ((y \in ⋃_{x \in A} B \land z \in ⋃_{x \in A} B) \land (F (y) R F (z) \lor (F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z)))\} = \{⟨o, p⟩ \| ((o \in ⋃_{l \in A} ⦋ l / x ⦌ B \land p \in ⋃_{l \in A} ⦋ l / x ⦌ B) \land (F (o) R F (p) \lor (F (o) = F (p) \land o ⦋ F (o) / l ⦌ ⦋ l / x ⦌ S p)))\}$
48	2 47	eqtri	$⊢ T = \{⟨o, p⟩ \| ((o \in ⋃_{l \in A} ⦋ l / x ⦌ B \land p \in ⋃_{l \in A} ⦋ l / x ⦌ B) \land (F (o) R F (p) \lor (F (o) = F (p) \land o ⦋ F (o) / l ⦌ ⦋ l / x ⦌ S p)))\}$
49		breq1	$⊢ q = t \to (q R s \leftrightarrow t R s)$
50	49	notbid	$⊢ q = t \to (\neg q R s \leftrightarrow \neg t R s)$
51	50	cbvralvw	$⊢ \forall q \in F [r] \neg q R s \leftrightarrow \forall t \in F [r] \neg t R s$
52	51	a1i	$⊢ s \in F [r] \to (\forall q \in F [r] \neg q R s \leftrightarrow \forall t \in F [r] \neg t R s)$
53	52	riotabiia	$⊢ (ι s \in F [r] \| \forall q \in F [r] \neg q R s) = (ι s \in F [r] \| \forall t \in F [r] \neg t R s)$
54	29 48 53	weiunfrlem2	$⊢ (R We A \land R Se A \land \forall l \in A ⦋ l / x ⦌ S Fr ⦋ l / x ⦌ B) \to T Fr ⋃_{l \in A} ⦋ l / x ⦌ B$
55		nfv	$⊢ Ⅎ l S Fr B$
56		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ l / x ⦌ S$
57	56 10	nffr	$⊢ Ⅎ x ⦋ l / x ⦌ S Fr ⦋ l / x ⦌ B$
58		csbeq1a	$⊢ x = l \to S = ⦋ l / x ⦌ S$
59		freq1	$⊢ S = ⦋ l / x ⦌ S \to (S Fr B \leftrightarrow ⦋ l / x ⦌ S Fr B)$
60	58 59	syl	$⊢ x = l \to (S Fr B \leftrightarrow ⦋ l / x ⦌ S Fr B)$
61		freq2	$⊢ B = ⦋ l / x ⦌ B \to (⦋ l / x ⦌ S Fr B \leftrightarrow ⦋ l / x ⦌ S Fr ⦋ l / x ⦌ B)$
62	12 61	syl	$⊢ x = l \to (⦋ l / x ⦌ S Fr B \leftrightarrow ⦋ l / x ⦌ S Fr ⦋ l / x ⦌ B)$
63	60 62	bitrd	$⊢ x = l \to (S Fr B \leftrightarrow ⦋ l / x ⦌ S Fr ⦋ l / x ⦌ B)$
64	55 57 63	cbvralw	$⊢ \forall x \in A S Fr B \leftrightarrow \forall l \in A ⦋ l / x ⦌ S Fr ⦋ l / x ⦌ B$
65	64	3anbi3i	$⊢ (R We A \land R Se A \land \forall x \in A S Fr B) \leftrightarrow (R We A \land R Se A \land \forall l \in A ⦋ l / x ⦌ S Fr ⦋ l / x ⦌ B)$
66		freq2	$⊢ ⋃_{x \in A} B = ⋃_{l \in A} ⦋ l / x ⦌ B \to (T Fr ⋃_{x \in A} B \leftrightarrow T Fr ⋃_{l \in A} ⦋ l / x ⦌ B)$
67	27 66	ax-mp	$⊢ T Fr ⋃_{x \in A} B \leftrightarrow T Fr ⋃_{l \in A} ⦋ l / x ⦌ B$
68	54 65 67	3imtr4i	$⊢ (R We A \land R Se A \land \forall x \in A S Fr B) \to T Fr ⋃_{x \in A} B$

Metamath Proof Explorer

Theorem weiunfr

Proof