weiunfrlem1

	Ref	Expression
Hypotheses	weiunfrlem1.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))$
	weiunfrlem1.2	$⊢ C = (ι s \in F [r] \| \forall t \in F [r] \neg t R s)$
Assertion	weiunfrlem1	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to (C \in F [r] \land \forall w \in r \neg F (w) R C)$

Proof

Step	Hyp	Ref	Expression
1		weiunfrlem1.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		weiunfrlem1.2	$⊢ C = (ι s \in F [r] \| \forall t \in F [r] \neg t R s)$
3		simpl	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to (R We A \land R Se A)$
4	1	weiunlem1	$⊢ (R We A \land R Se A) \to (F : ⋃_{x \in A} B ⟶ A \land \forall w \in ⋃_{x \in A} B w \in ⦋ F (w) / x ⦌ B \land \forall w \in ⋃_{x \in A} B \forall v \in A (w \in ⦋ v / x ⦌ B \to \neg v R F (w)))$
5	4	adantr	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to (F : ⋃_{x \in A} B ⟶ A \land \forall w \in ⋃_{x \in A} B w \in ⦋ F (w) / x ⦌ B \land \forall w \in ⋃_{x \in A} B \forall v \in A (w \in ⦋ v / x ⦌ B \to \neg v R F (w)))$
6	5	simp1d	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to F : ⋃_{x \in A} B ⟶ A$
7	6	fimassd	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to F [r] \subseteq A$
8		simprl	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to r \subseteq ⋃_{x \in A} B$
9	6	fdmd	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to dom F = ⋃_{x \in A} B$
10	8 9	sseqtrrd	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to r \subseteq dom F$
11		sseqin2	$⊢ r \subseteq dom F \leftrightarrow dom F \cap r = r$
12	10 11	sylib	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to dom F \cap r = r$
13		simprr	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to r \neq \emptyset$
14	12 13	eqnetrd	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to dom F \cap r \neq \emptyset$
15	14	imadisjlnd	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to F [r] \neq \emptyset$
16		wereu2	$⊢ ((R We A \land R Se A) \land (F [r] \subseteq A \land F [r] \neq \emptyset)) \to \exists! s \in F [r] \forall t \in F [r] \neg t R s$
17	3 7 15 16	syl12anc	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to \exists! s \in F [r] \forall t \in F [r] \neg t R s$
18		riotacl2	$⊢ \exists! s \in F [r] \forall t \in F [r] \neg t R s \to (ι s \in F [r] \| \forall t \in F [r] \neg t R s) \in \{s \in F [r] \| \forall t \in F [r] \neg t R s\}$
19	17 18	syl	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to (ι s \in F [r] \| \forall t \in F [r] \neg t R s) \in \{s \in F [r] \| \forall t \in F [r] \neg t R s\}$
20	2 19	eqeltrid	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to C \in \{s \in F [r] \| \forall t \in F [r] \neg t R s\}$
21	6	ffnd	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to F Fn ⋃_{x \in A} B$
22		breq1	$⊢ t = F (w) \to (t R s \leftrightarrow F (w) R s)$
23	22	notbid	$⊢ t = F (w) \to (\neg t R s \leftrightarrow \neg F (w) R s)$
24	23	ralima	$⊢ (F Fn ⋃_{x \in A} B \land r \subseteq ⋃_{x \in A} B) \to (\forall t \in F [r] \neg t R s \leftrightarrow \forall w \in r \neg F (w) R s)$
25	24	rabbidv	$⊢ (F Fn ⋃_{x \in A} B \land r \subseteq ⋃_{x \in A} B) \to \{s \in F [r] \| \forall t \in F [r] \neg t R s\} = \{s \in F [r] \| \forall w \in r \neg F (w) R s\}$
26	21 8 25	syl2anc	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to \{s \in F [r] \| \forall t \in F [r] \neg t R s\} = \{s \in F [r] \| \forall w \in r \neg F (w) R s\}$
27	20 26	eleqtrd	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to C \in \{s \in F [r] \| \forall w \in r \neg F (w) R s\}$
28		nfriota1	$⊢ \underline{Ⅎ} s (ι s \in F [r] \| \forall t \in F [r] \neg t R s)$
29	2 28	nfcxfr	$⊢ \underline{Ⅎ} s C$
30		nfcv	$⊢ \underline{Ⅎ} s F [r]$
31		nfcv	$⊢ \underline{Ⅎ} s r$
32		nfcv	$⊢ \underline{Ⅎ} s F (w)$
33		nfcv	$⊢ \underline{Ⅎ} s R$
34	32 33 29	nfbr	$⊢ Ⅎ s F (w) R C$
35	34	nfn	$⊢ Ⅎ s \neg F (w) R C$
36	31 35	nfralw	$⊢ Ⅎ s \forall w \in r \neg F (w) R C$
37		breq2	$⊢ s = C \to (F (w) R s \leftrightarrow F (w) R C)$
38	37	notbid	$⊢ s = C \to (\neg F (w) R s \leftrightarrow \neg F (w) R C)$
39	38	ralbidv	$⊢ s = C \to (\forall w \in r \neg F (w) R s \leftrightarrow \forall w \in r \neg F (w) R C)$
40	29 30 36 39	elrabf	$⊢ C \in \{s \in F [r] \| \forall w \in r \neg F (w) R s\} \leftrightarrow (C \in F [r] \land \forall w \in r \neg F (w) R C)$
41	27 40	sylib	$⊢ ((R We A \land R Se A) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to (C \in F [r] \land \forall w \in r \neg F (w) R C)$

Metamath Proof Explorer

Theorem weiunfrlem1

Proof