weiunse

Description: The relation constructed in weiunpo , weiunso , weiunfr , and weiunwe is set-like if all members of the indexed union are sets. (Contributed by Matthew House, 23-Aug-2025)

	Ref	Expression
Hypotheses	weiun.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))$
	weiun.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	weiunse	$⊢ (R We A \land R Se A \land \forall x \in A B \in V) \to T Se ⋃_{x \in A} B$

Proof

Step	Hyp	Ref	Expression
1		weiun.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		weiun.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		simpl2	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to R Se A$
4		simpl1	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to R We A$
5	1 2 4 3	weiunlem2	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to (F : ⋃_{x \in A} B ⟶ A \land \forall t \in ⋃_{x \in A} B t \in ⦋ F (t) / x ⦌ B \land \forall s \in A \forall t \in ⦋ s / x ⦌ B \neg s R F (t))$
6	5	simp1d	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to F : ⋃_{x \in A} B ⟶ A$
7		simpr	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to p \in ⋃_{x \in A} B$
8	6 7	ffvelcdmd	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to F (p) \in A$
9		seex	$⊢ (R Se A \land F (p) \in A) \to \{r \in A \| r R F (p)\} \in V$
10	3 8 9	syl2anc	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to \{r \in A \| r R F (p)\} \in V$
11		snex	$⊢ \{F (p)\} \in V$
12		unexg	$⊢ (\{r \in A \| r R F (p)\} \in V \land \{F (p)\} \in V) \to \{r \in A \| r R F (p)\} \cup \{F (p)\} \in V$
13	10 11 12	sylancl	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to \{r \in A \| r R F (p)\} \cup \{F (p)\} \in V$
14		ssrab2	$⊢ \{r \in A \| r R F (p)\} \subseteq A$
15	14	a1i	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to \{r \in A \| r R F (p)\} \subseteq A$
16	8	snssd	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to \{F (p)\} \subseteq A$
17	15 16	unssd	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to \{r \in A \| r R F (p)\} \cup \{F (p)\} \subseteq A$
18		simpl3	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to \forall x \in A B \in V$
19		elex	$⊢ B \in V \to B \in V$
20	19	ralimi	$⊢ \forall x \in A B \in V \to \forall x \in A B \in V$
21	18 20	syl	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to \forall x \in A B \in V$
22		nfv	$⊢ Ⅎ s B \in V$
23		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ B$
24	23	nfel1	$⊢ Ⅎ x ⦋ s / x ⦌ B \in V$
25		csbeq1a	$⊢ x = s \to B = ⦋ s / x ⦌ B$
26	25	eleq1d	$⊢ x = s \to (B \in V \leftrightarrow ⦋ s / x ⦌ B \in V)$
27	22 24 26	cbvralw	$⊢ \forall x \in A B \in V \leftrightarrow \forall s \in A ⦋ s / x ⦌ B \in V$
28	21 27	sylib	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to \forall s \in A ⦋ s / x ⦌ B \in V$
29		ssralv	$⊢ \{r \in A \| r R F (p)\} \cup \{F (p)\} \subseteq A \to (\forall s \in A ⦋ s / x ⦌ B \in V \to \forall s \in (\{r \in A \| r R F (p)\} \cup \{F (p)\}) ⦋ s / x ⦌ B \in V)$
30	17 28 29	sylc	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to \forall s \in (\{r \in A \| r R F (p)\} \cup \{F (p)\}) ⦋ s / x ⦌ B \in V$
31		iunexg	$⊢ (\{r \in A \| r R F (p)\} \cup \{F (p)\} \in V \land \forall s \in (\{r \in A \| r R F (p)\} \cup \{F (p)\}) ⦋ s / x ⦌ B \in V) \to ⋃_{s \in \{r \in A \| r R F (p)\} \cup \{F (p)\}} ⦋ s / x ⦌ B \in V$
32	13 30 31	syl2anc	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to ⋃_{s \in \{r \in A \| r R F (p)\} \cup \{F (p)\}} ⦋ s / x ⦌ B \in V$
33	6	3ad2ant1	$⊢ (((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \land q \in ⋃_{x \in A} B \land q T p) \to F : ⋃_{x \in A} B ⟶ A$
34		simp2	$⊢ (((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \land q \in ⋃_{x \in A} B \land q T p) \to q \in ⋃_{x \in A} B$
35	33 34	ffvelcdmd	$⊢ (((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \land q \in ⋃_{x \in A} B \land q T p) \to F (q) \in A$
36		breq1	$⊢ r = F (q) \to (r R F (p) \leftrightarrow F (q) R F (p))$
37	36	elrab	$⊢ F (q) \in \{r \in A \| r R F (p)\} \leftrightarrow (F (q) \in A \land F (q) R F (p))$
38		elun1	$⊢ F (q) \in \{r \in A \| r R F (p)\} \to F (q) \in (\{r \in A \| r R F (p)\} \cup \{F (p)\})$
39	37 38	sylbir	$⊢ (F (q) \in A \land F (q) R F (p)) \to F (q) \in (\{r \in A \| r R F (p)\} \cup \{F (p)\})$
40	35 39	sylan	$⊢ ((((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \land q \in ⋃_{x \in A} B \land q T p) \land F (q) R F (p)) \to F (q) \in (\{r \in A \| r R F (p)\} \cup \{F (p)\})$
41		fvex	$⊢ F (q) \in V$
42	41	elsn	$⊢ F (q) \in \{F (p)\} \leftrightarrow F (q) = F (p)$
43		elun2	$⊢ F (q) \in \{F (p)\} \to F (q) \in (\{r \in A \| r R F (p)\} \cup \{F (p)\})$
44	42 43	sylbir	$⊢ F (q) = F (p) \to F (q) \in (\{r \in A \| r R F (p)\} \cup \{F (p)\})$
45	44	ad2antrl	$⊢ ((((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \land q \in ⋃_{x \in A} B \land q T p) \land (F (q) = F (p) \land q ⦋ F (q) / x ⦌ S p)) \to F (q) \in (\{r \in A \| r R F (p)\} \cup \{F (p)\})$
46	1 2	weiunlem1	$⊢ q T p \leftrightarrow ((q \in ⋃_{x \in A} B \land p \in ⋃_{x \in A} B) \land (F (q) R F (p) \lor (F (q) = F (p) \land q ⦋ F (q) / x ⦌ S p)))$
47	46	simprbi	$⊢ q T p \to (F (q) R F (p) \lor (F (q) = F (p) \land q ⦋ F (q) / x ⦌ S p))$
48	47	3ad2ant3	$⊢ (((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \land q \in ⋃_{x \in A} B \land q T p) \to (F (q) R F (p) \lor (F (q) = F (p) \land q ⦋ F (q) / x ⦌ S p))$
49	40 45 48	mpjaodan	$⊢ (((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \land q \in ⋃_{x \in A} B \land q T p) \to F (q) \in (\{r \in A \| r R F (p)\} \cup \{F (p)\})$
50		id	$⊢ t = q \to t = q$
51		fveq2	$⊢ t = q \to F (t) = F (q)$
52	51	csbeq1d	$⊢ t = q \to ⦋ F (t) / x ⦌ B = ⦋ F (q) / x ⦌ B$
53	50 52	eleq12d	$⊢ t = q \to (t \in ⦋ F (t) / x ⦌ B \leftrightarrow q \in ⦋ F (q) / x ⦌ B)$
54	5	simp2d	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to \forall t \in ⋃_{x \in A} B t \in ⦋ F (t) / x ⦌ B$
55	54	3ad2ant1	$⊢ (((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \land q \in ⋃_{x \in A} B \land q T p) \to \forall t \in ⋃_{x \in A} B t \in ⦋ F (t) / x ⦌ B$
56	53 55 34	rspcdva	$⊢ (((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \land q \in ⋃_{x \in A} B \land q T p) \to q \in ⦋ F (q) / x ⦌ B$
57		csbeq1	$⊢ s = F (q) \to ⦋ s / x ⦌ B = ⦋ F (q) / x ⦌ B$
58	57	eliuni	$⊢ (F (q) \in (\{r \in A \| r R F (p)\} \cup \{F (p)\}) \land q \in ⦋ F (q) / x ⦌ B) \to q \in ⋃_{s \in \{r \in A \| r R F (p)\} \cup \{F (p)\}} ⦋ s / x ⦌ B$
59	49 56 58	syl2anc	$⊢ (((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \land q \in ⋃_{x \in A} B \land q T p) \to q \in ⋃_{s \in \{r \in A \| r R F (p)\} \cup \{F (p)\}} ⦋ s / x ⦌ B$
60	59	rabssdv	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to \{q \in ⋃_{x \in A} B \| q T p\} \subseteq ⋃_{s \in \{r \in A \| r R F (p)\} \cup \{F (p)\}} ⦋ s / x ⦌ B$
61	32 60	ssexd	$⊢ ((R We A \land R Se A \land \forall x \in A B \in V) \land p \in ⋃_{x \in A} B) \to \{q \in ⋃_{x \in A} B \| q T p\} \in V$
62	61	ralrimiva	$⊢ (R We A \land R Se A \land \forall x \in A B \in V) \to \forall p \in ⋃_{x \in A} B \{q \in ⋃_{x \in A} B \| q T p\} \in V$
63		df-se	$⊢ T Se ⋃_{x \in A} B \leftrightarrow \forall p \in ⋃_{x \in A} B \{q \in ⋃_{x \in A} B \| q T p\} \in V$
64	62 63	sylibr	$⊢ (R We A \land R Se A \land \forall x \in A B \in V) \to T Se ⋃_{x \in A} B$

Metamath Proof Explorer

Theorem weiunse

Proof