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	weiunse.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))$
	weiunse.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		weiunse.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		weiunse.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	weiunlem2	$⊢ (R We A \land R Se A) \to (F : ⋃_{x \in A} B ⟶ A \land \forall t \in ⋃_{x \in A} B t \in ⦋ F (t) / x ⦌ B \land \forall t \in ⋃_{x \in A} B \forall s \in A (t \in ⦋ s / x ⦌ B \to \neg s R F (t)))$
6	4 3 5	syl2anc	$⊢ ((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 t \in ⋃_{x \in A} B \forall s \in A (t \in ⦋ s / x ⦌ B \to \neg s R F (t)))$
7	6	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$
8		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$
9	7 8	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$
10		seex	$⊢ (R Se A \land F (p) \in A) \to \{r \in A \| r R F (p)\} \in V$
11	3 9 10	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$
12		snex	$⊢ \{F (p)\} \in V$
13		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$
14	11 12 13	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$
15		ssrab2	$⊢ \{r \in A \| r R F (p)\} \subseteq A$
16	15	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$
17	9	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$
18	16 17	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$
19		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$
20		elex	$⊢ B \in V \to B \in V$
21	20	ralimi	$⊢ \forall x \in A B \in V \to \forall x \in A B \in V$
22	19 21	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$
23		nfv	$⊢ Ⅎ s B \in V$
24		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ B$
25	24	nfel1	$⊢ Ⅎ x ⦋ s / x ⦌ B \in V$
26		csbeq1a	$⊢ x = s \to B = ⦋ s / x ⦌ B$
27	26	eleq1d	$⊢ x = s \to (B \in V \leftrightarrow ⦋ s / x ⦌ B \in V)$
28	23 25 27	cbvralw	$⊢ \forall x \in A B \in V \leftrightarrow \forall s \in A ⦋ s / x ⦌ B \in V$
29	22 28	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$
30		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)$
31	18 29 30	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$
32		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$
33	14 31 32	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$
34	7	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$
35		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$
36	34 35	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$
37		breq1	$⊢ r = F (q) \to (r R F (p) \leftrightarrow F (q) R F (p))$
38	37	elrab	$⊢ F (q) \in \{r \in A \| r R F (p)\} \leftrightarrow (F (q) \in A \land F (q) R F (p))$
39		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)\})$
40	38 39	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)\})$
41	36 40	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)\})$
42		fvex	$⊢ F (q) \in V$
43	42	elsn	$⊢ F (q) \in \{F (p)\} \leftrightarrow F (q) = F (p)$
44		elun2	$⊢ F (q) \in \{F (p)\} \to F (q) \in (\{r \in A \| r R F (p)\} \cup \{F (p)\})$
45	43 44	sylbir	$⊢ F (q) = F (p) \to F (q) \in (\{r \in A \| r R F (p)\} \cup \{F (p)\})$
46	45	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)\})$
47		simpl	$⊢ (y = q \land z = p) \to y = q$
48	47	fveq2d	$⊢ (y = q \land z = p) \to F (y) = F (q)$
49		simpr	$⊢ (y = q \land z = p) \to z = p$
50	49	fveq2d	$⊢ (y = q \land z = p) \to F (z) = F (p)$
51	48 50	breq12d	$⊢ (y = q \land z = p) \to (F (y) R F (z) \leftrightarrow F (q) R F (p))$
52	48 50	eqeq12d	$⊢ (y = q \land z = p) \to (F (y) = F (z) \leftrightarrow F (q) = F (p))$
53	48	csbeq1d	$⊢ (y = q \land z = p) \to ⦋ F (y) / x ⦌ S = ⦋ F (q) / x ⦌ S$
54	47 53 49	breq123d	$⊢ (y = q \land z = p) \to (y ⦋ F (y) / x ⦌ S z \leftrightarrow q ⦋ F (q) / x ⦌ S p)$
55	52 54	anbi12d	$⊢ (y = q \land z = p) \to ((F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z) \leftrightarrow (F (q) = F (p) \land q ⦋ F (q) / x ⦌ S p))$
56	51 55	orbi12d	$⊢ (y = q \land z = p) \to ((F (y) R F (z) \lor (F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z)) \leftrightarrow (F (q) R F (p) \lor (F (q) = F (p) \land q ⦋ F (q) / x ⦌ S p)))$
57	56 2	brab2a	$⊢ 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)))$
58	57	simprbi	$⊢ q T p \to (F (q) R F (p) \lor (F (q) = F (p) \land q ⦋ F (q) / x ⦌ S p))$
59	58	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))$
60	41 46 59	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)\})$
61		id	$⊢ t = q \to t = q$
62		fveq2	$⊢ t = q \to F (t) = F (q)$
63	62	csbeq1d	$⊢ t = q \to ⦋ F (t) / x ⦌ B = ⦋ F (q) / x ⦌ B$
64	61 63	eleq12d	$⊢ t = q \to (t \in ⦋ F (t) / x ⦌ B \leftrightarrow q \in ⦋ F (q) / x ⦌ B)$
65	6	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$
66	65	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$
67	64 66 35	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$
68		csbeq1	$⊢ s = F (q) \to ⦋ s / x ⦌ B = ⦋ F (q) / x ⦌ B$
69	68	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$
70	60 67 69	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$
71	70	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$
72	33 71	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$
73	72	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$
74		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$
75	73 74	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