weiunfrlem2

	Ref	Expression
Hypotheses	weiunfrlem2.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))$
	weiunfrlem2.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)))\}$
	weiunfrlem2.3	$⊢ C = (ι s \in F [r] \| \forall t \in F [r] \neg t R s)$
Assertion	weiunfrlem2	$⊢ (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		weiunfrlem2.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		weiunfrlem2.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		weiunfrlem2.3	$⊢ C = (ι s \in F [r] \| \forall t \in F [r] \neg t R s)$
4		vex	$⊢ r \in V$
5	4	inex1	$⊢ r \cap ⦋ C / x ⦌ B \in V$
6	5	a1i	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to r \cap ⦋ C / x ⦌ B \in V$
7	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)))$
8	7	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)))$
9	8	3adantl3	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \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)))$
10	9	simp1d	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to F : ⋃_{x \in A} B ⟶ A$
11	10	fimassd	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to F [r] \subseteq A$
12	1 3	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)$
13	12	3adantl3	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \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)$
14	13	simpld	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to C \in F [r]$
15	11 14	sseldd	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to C \in A$
16		simpl3	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to \forall x \in A S Fr B$
17		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} B$
18		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| w \in B\}$
19		nfv	$⊢ Ⅎ x \neg v R u$
20	18 19	nfralw	$⊢ Ⅎ x \forall v \in \{x \in A \| w \in B\} \neg v R u$
21	20 18	nfriota	$⊢ \underline{Ⅎ} x (ι u \in \{x \in A \| w \in B\} \| \forall v \in \{x \in A \| w \in B\} \neg v R u)$
22	17 21	nfmpt	$⊢ \underline{Ⅎ} x (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))$
23	1 22	nfcxfr	$⊢ \underline{Ⅎ} x F$
24		nfcv	$⊢ \underline{Ⅎ} x r$
25	23 24	nfima	$⊢ \underline{Ⅎ} x F [r]$
26		nfv	$⊢ Ⅎ x \neg t R s$
27	25 26	nfralw	$⊢ Ⅎ x \forall t \in F [r] \neg t R s$
28	27 25	nfriota	$⊢ \underline{Ⅎ} x (ι s \in F [r] \| \forall t \in F [r] \neg t R s)$
29	3 28	nfcxfr	$⊢ \underline{Ⅎ} x C$
30		nfra1	$⊢ Ⅎ x \forall x \in A S Fr B$
31	29	nfcsb1	$⊢ \underline{Ⅎ} x ⦋ C / x ⦌ S$
32	29	nfcsb1	$⊢ \underline{Ⅎ} x ⦋ C / x ⦌ B$
33	31 32	nffr	$⊢ Ⅎ x ⦋ C / x ⦌ S Fr ⦋ C / x ⦌ B$
34	30 33	nfim	$⊢ Ⅎ x (\forall x \in A S Fr B \to ⦋ C / x ⦌ S Fr ⦋ C / x ⦌ B)$
35		csbeq1a	$⊢ x = C \to S = ⦋ C / x ⦌ S$
36		freq1	$⊢ S = ⦋ C / x ⦌ S \to (S Fr B \leftrightarrow ⦋ C / x ⦌ S Fr B)$
37	35 36	syl	$⊢ x = C \to (S Fr B \leftrightarrow ⦋ C / x ⦌ S Fr B)$
38		csbeq1a	$⊢ x = C \to B = ⦋ C / x ⦌ B$
39		freq2	$⊢ B = ⦋ C / x ⦌ B \to (⦋ C / x ⦌ S Fr B \leftrightarrow ⦋ C / x ⦌ S Fr ⦋ C / x ⦌ B)$
40	38 39	syl	$⊢ x = C \to (⦋ C / x ⦌ S Fr B \leftrightarrow ⦋ C / x ⦌ S Fr ⦋ C / x ⦌ B)$
41	37 40	bitrd	$⊢ x = C \to (S Fr B \leftrightarrow ⦋ C / x ⦌ S Fr ⦋ C / x ⦌ B)$
42	41	imbi2d	$⊢ x = C \to ((\forall x \in A S Fr B \to S Fr B) \leftrightarrow (\forall x \in A S Fr B \to ⦋ C / x ⦌ S Fr ⦋ C / x ⦌ B))$
43		rsp	$⊢ \forall x \in A S Fr B \to (x \in A \to S Fr B)$
44	43	com12	$⊢ x \in A \to (\forall x \in A S Fr B \to S Fr B)$
45	29 34 42 44	vtoclgaf	$⊢ C \in A \to (\forall x \in A S Fr B \to ⦋ C / x ⦌ S Fr ⦋ C / x ⦌ B)$
46	15 16 45	sylc	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to ⦋ C / x ⦌ S Fr ⦋ C / x ⦌ B$
47		inss2	$⊢ r \cap ⦋ C / x ⦌ B \subseteq ⦋ C / x ⦌ B$
48	47	a1i	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to r \cap ⦋ C / x ⦌ B \subseteq ⦋ C / x ⦌ B$
49	10	ffund	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to Fun F$
50		fvelima	$⊢ (Fun F \land C \in F [r]) \to \exists o \in r F (o) = C$
51	49 14 50	syl2anc	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to \exists o \in r F (o) = C$
52		simprl	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (o \in r \land F (o) = C)) \to o \in r$
53		simplrl	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (o \in r \land F (o) = C)) \to r \subseteq ⋃_{x \in A} B$
54	53 52	sseldd	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (o \in r \land F (o) = C)) \to o \in ⋃_{x \in A} B$
55	9	simp2d	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to \forall w \in ⋃_{x \in A} B w \in ⦋ F (w) / x ⦌ B$
56	55	adantr	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (o \in r \land F (o) = C)) \to \forall w \in ⋃_{x \in A} B w \in ⦋ F (w) / x ⦌ B$
57		id	$⊢ w = o \to w = o$
58		fveq2	$⊢ w = o \to F (w) = F (o)$
59	58	csbeq1d	$⊢ w = o \to ⦋ F (w) / x ⦌ B = ⦋ F (o) / x ⦌ B$
60	57 59	eleq12d	$⊢ w = o \to (w \in ⦋ F (w) / x ⦌ B \leftrightarrow o \in ⦋ F (o) / x ⦌ B)$
61	60	rspcv	$⊢ o \in ⋃_{x \in A} B \to (\forall w \in ⋃_{x \in A} B w \in ⦋ F (w) / x ⦌ B \to o \in ⦋ F (o) / x ⦌ B)$
62	54 56 61	sylc	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (o \in r \land F (o) = C)) \to o \in ⦋ F (o) / x ⦌ B$
63		csbeq1	$⊢ F (o) = C \to ⦋ F (o) / x ⦌ B = ⦋ C / x ⦌ B$
64	63	ad2antll	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (o \in r \land F (o) = C)) \to ⦋ F (o) / x ⦌ B = ⦋ C / x ⦌ B$
65	62 64	eleqtrd	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (o \in r \land F (o) = C)) \to o \in ⦋ C / x ⦌ B$
66	52 65	elind	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (o \in r \land F (o) = C)) \to o \in (r \cap ⦋ C / x ⦌ B)$
67	66	ne0d	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (o \in r \land F (o) = C)) \to r \cap ⦋ C / x ⦌ B \neq \emptyset$
68	51 67	rexlimddv	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to r \cap ⦋ C / x ⦌ B \neq \emptyset$
69		fri	$⊢ ((r \cap ⦋ C / x ⦌ B \in V \land ⦋ C / x ⦌ S Fr ⦋ C / x ⦌ B) \land (r \cap ⦋ C / x ⦌ B \subseteq ⦋ C / x ⦌ B \land r \cap ⦋ C / x ⦌ B \neq \emptyset)) \to \exists p \in (r \cap ⦋ C / x ⦌ B) \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p$
70	6 46 48 68 69	syl22anc	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to \exists p \in (r \cap ⦋ C / x ⦌ B) \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p$
71		simprl	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to p \in (r \cap ⦋ C / x ⦌ B)$
72	71	elin1d	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to p \in r$
73	13	adantr	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to (C \in F [r] \land \forall w \in r \neg F (w) R C)$
74	73	simprd	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to \forall w \in r \neg F (w) R C$
75		fveq2	$⊢ w = t \to F (w) = F (t)$
76	75	breq1d	$⊢ w = t \to (F (w) R C \leftrightarrow F (t) R C)$
77	76	notbid	$⊢ w = t \to (\neg F (w) R C \leftrightarrow \neg F (t) R C)$
78	77	rspcv	$⊢ t \in r \to (\forall w \in r \neg F (w) R C \to \neg F (t) R C)$
79	74 78	mpan9	$⊢ ((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \to \neg F (t) R C$
80		fveq2	$⊢ w = p \to F (w) = F (p)$
81	80	breq1d	$⊢ w = p \to (F (w) R C \leftrightarrow F (p) R C)$
82	81	notbid	$⊢ w = p \to (\neg F (w) R C \leftrightarrow \neg F (p) R C)$
83	82	rspcv	$⊢ p \in r \to (\forall w \in r \neg F (w) R C \to \neg F (p) R C)$
84	72 74 83	sylc	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to \neg F (p) R C$
85	9	adantr	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \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)))$
86	85	simp3d	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to \forall w \in ⋃_{x \in A} B \forall v \in A (w \in ⦋ v / x ⦌ B \to \neg v R F (w))$
87	71	elin2d	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to p \in ⦋ C / x ⦌ B$
88		simplrl	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to r \subseteq ⋃_{x \in A} B$
89	88 72	sseldd	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to p \in ⋃_{x \in A} B$
90	15	adantr	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to C \in A$
91		simpl	$⊢ (w = p \land v = C) \to w = p$
92		simpr	$⊢ (w = p \land v = C) \to v = C$
93	92	csbeq1d	$⊢ (w = p \land v = C) \to ⦋ v / x ⦌ B = ⦋ C / x ⦌ B$
94	91 93	eleq12d	$⊢ (w = p \land v = C) \to (w \in ⦋ v / x ⦌ B \leftrightarrow p \in ⦋ C / x ⦌ B)$
95	91	fveq2d	$⊢ (w = p \land v = C) \to F (w) = F (p)$
96	92 95	breq12d	$⊢ (w = p \land v = C) \to (v R F (w) \leftrightarrow C R F (p))$
97	96	notbid	$⊢ (w = p \land v = C) \to (\neg v R F (w) \leftrightarrow \neg C R F (p))$
98	94 97	imbi12d	$⊢ (w = p \land v = C) \to ((w \in ⦋ v / x ⦌ B \to \neg v R F (w)) \leftrightarrow (p \in ⦋ C / x ⦌ B \to \neg C R F (p)))$
99	98	rspc2gv	$⊢ (p \in ⋃_{x \in A} B \land C \in A) \to (\forall w \in ⋃_{x \in A} B \forall v \in A (w \in ⦋ v / x ⦌ B \to \neg v R F (w)) \to (p \in ⦋ C / x ⦌ B \to \neg C R F (p)))$
100	89 90 99	syl2anc	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to (\forall w \in ⋃_{x \in A} B \forall v \in A (w \in ⦋ v / x ⦌ B \to \neg v R F (w)) \to (p \in ⦋ C / x ⦌ B \to \neg C R F (p)))$
101	86 87 100	mp2d	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to \neg C R F (p)$
102		simpll1	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to R We A$
103		weso	$⊢ R We A \to R Or A$
104	102 103	syl	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to R Or A$
105	10	adantr	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to F : ⋃_{x \in A} B ⟶ A$
106	105 89	ffvelcdmd	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to F (p) \in A$
107		sotrieq2	$⊢ (R Or A \land (F (p) \in A \land C \in A)) \to (F (p) = C \leftrightarrow (\neg F (p) R C \land \neg C R F (p)))$
108	104 106 90 107	syl12anc	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to (F (p) = C \leftrightarrow (\neg F (p) R C \land \neg C R F (p)))$
109	84 101 108	mpbir2and	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to F (p) = C$
110	109	adantr	$⊢ ((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \to F (p) = C$
111		breq2	$⊢ F (p) = C \to (F (t) R F (p) \leftrightarrow F (t) R C)$
112	111	notbid	$⊢ F (p) = C \to (\neg F (t) R F (p) \leftrightarrow \neg F (t) R C)$
113	110 112	syl	$⊢ ((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \to (\neg F (t) R F (p) \leftrightarrow \neg F (t) R C)$
114	79 113	mpbird	$⊢ ((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \to \neg F (t) R F (p)$
115		simplr	$⊢ (((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \land F (t) = F (p)) \to t \in r$
116	88	sselda	$⊢ ((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \to t \in ⋃_{x \in A} B$
117	55	ad2antrr	$⊢ ((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \to \forall w \in ⋃_{x \in A} B w \in ⦋ F (w) / x ⦌ B$
118		id	$⊢ w = t \to w = t$
119	75	csbeq1d	$⊢ w = t \to ⦋ F (w) / x ⦌ B = ⦋ F (t) / x ⦌ B$
120	118 119	eleq12d	$⊢ w = t \to (w \in ⦋ F (w) / x ⦌ B \leftrightarrow t \in ⦋ F (t) / x ⦌ B)$
121	120	rspcv	$⊢ t \in ⋃_{x \in A} B \to (\forall w \in ⋃_{x \in A} B w \in ⦋ F (w) / x ⦌ B \to t \in ⦋ F (t) / x ⦌ B)$
122	116 117 121	sylc	$⊢ ((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \to t \in ⦋ F (t) / x ⦌ B$
123	122	adantr	$⊢ (((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \land F (t) = F (p)) \to t \in ⦋ F (t) / x ⦌ B$
124		simpr	$⊢ (((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \land F (t) = F (p)) \to F (t) = F (p)$
125	110	adantr	$⊢ (((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \land F (t) = F (p)) \to F (p) = C$
126	124 125	eqtrd	$⊢ (((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \land F (t) = F (p)) \to F (t) = C$
127	126	csbeq1d	$⊢ (((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \land F (t) = F (p)) \to ⦋ F (t) / x ⦌ B = ⦋ C / x ⦌ B$
128	123 127	eleqtrd	$⊢ (((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \land F (t) = F (p)) \to t \in ⦋ C / x ⦌ B$
129	115 128	elind	$⊢ (((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \land F (t) = F (p)) \to t \in (r \cap ⦋ C / x ⦌ B)$
130		simprr	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p$
131	130	ad2antrr	$⊢ (((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \land F (t) = F (p)) \to \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p$
132		breq1	$⊢ q = t \to (q ⦋ C / x ⦌ S p \leftrightarrow t ⦋ C / x ⦌ S p)$
133	132	notbid	$⊢ q = t \to (\neg q ⦋ C / x ⦌ S p \leftrightarrow \neg t ⦋ C / x ⦌ S p)$
134	133	rspcv	$⊢ t \in (r \cap ⦋ C / x ⦌ B) \to (\forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p \to \neg t ⦋ C / x ⦌ S p)$
135	129 131 134	sylc	$⊢ (((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \land F (t) = F (p)) \to \neg t ⦋ C / x ⦌ S p$
136	126	csbeq1d	$⊢ (((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \land F (t) = F (p)) \to ⦋ F (t) / x ⦌ S = ⦋ C / x ⦌ S$
137	136	breqd	$⊢ (((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \land F (t) = F (p)) \to (t ⦋ F (t) / x ⦌ S p \leftrightarrow t ⦋ C / x ⦌ S p)$
138	135 137	mtbird	$⊢ (((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \land F (t) = F (p)) \to \neg t ⦋ F (t) / x ⦌ S p$
139	138	ex	$⊢ ((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \to (F (t) = F (p) \to \neg t ⦋ F (t) / x ⦌ S p)$
140		imnan	$⊢ (F (t) = F (p) \to \neg t ⦋ F (t) / x ⦌ S p) \leftrightarrow \neg (F (t) = F (p) \land t ⦋ F (t) / x ⦌ S p)$
141	139 140	sylib	$⊢ ((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \to \neg (F (t) = F (p) \land t ⦋ F (t) / x ⦌ S p)$
142		pm4.56	$⊢ (\neg F (t) R F (p) \land \neg (F (t) = F (p) \land t ⦋ F (t) / x ⦌ S p)) \leftrightarrow \neg (F (t) R F (p) \lor (F (t) = F (p) \land t ⦋ F (t) / x ⦌ S p))$
143	142	biimpi	$⊢ (\neg F (t) R F (p) \land \neg (F (t) = F (p) \land t ⦋ F (t) / x ⦌ S p)) \to \neg (F (t) R F (p) \lor (F (t) = F (p) \land t ⦋ F (t) / x ⦌ S p))$
144	114 141 143	syl2anc	$⊢ ((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \to \neg (F (t) R F (p) \lor (F (t) = F (p) \land t ⦋ F (t) / x ⦌ S p))$
145	144	intnand	$⊢ ((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \to \neg ((t \in ⋃_{x \in A} B \land p \in ⋃_{x \in A} B) \land (F (t) R F (p) \lor (F (t) = F (p) \land t ⦋ F (t) / x ⦌ S p)))$
146		simpl	$⊢ (y = t \land z = p) \to y = t$
147	146	fveq2d	$⊢ (y = t \land z = p) \to F (y) = F (t)$
148		simpr	$⊢ (y = t \land z = p) \to z = p$
149	148	fveq2d	$⊢ (y = t \land z = p) \to F (z) = F (p)$
150	147 149	breq12d	$⊢ (y = t \land z = p) \to (F (y) R F (z) \leftrightarrow F (t) R F (p))$
151	147 149	eqeq12d	$⊢ (y = t \land z = p) \to (F (y) = F (z) \leftrightarrow F (t) = F (p))$
152	147	csbeq1d	$⊢ (y = t \land z = p) \to ⦋ F (y) / x ⦌ S = ⦋ F (t) / x ⦌ S$
153	146 152 148	breq123d	$⊢ (y = t \land z = p) \to (y ⦋ F (y) / x ⦌ S z \leftrightarrow t ⦋ F (t) / x ⦌ S p)$
154	151 153	anbi12d	$⊢ (y = t \land z = p) \to ((F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z) \leftrightarrow (F (t) = F (p) \land t ⦋ F (t) / x ⦌ S p))$
155	150 154	orbi12d	$⊢ (y = t \land z = p) \to ((F (y) R F (z) \lor (F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z)) \leftrightarrow (F (t) R F (p) \lor (F (t) = F (p) \land t ⦋ F (t) / x ⦌ S p)))$
156	155 2	brab2a	$⊢ t T p \leftrightarrow ((t \in ⋃_{x \in A} B \land p \in ⋃_{x \in A} B) \land (F (t) R F (p) \lor (F (t) = F (p) \land t ⦋ F (t) / x ⦌ S p)))$
157	145 156	sylnibr	$⊢ ((((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \land t \in r) \to \neg t T p$
158	157	ralrimiva	$⊢ (((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \land (p \in (r \cap ⦋ C / x ⦌ B) \land \forall q \in (r \cap ⦋ C / x ⦌ B) \neg q ⦋ C / x ⦌ S p)) \to \forall t \in r \neg t T p$
159	70 72 158	reximssdv	$⊢ ((R We A \land R Se A \land \forall x \in A S Fr B) \land (r \subseteq ⋃_{x \in A} B \land r \neq \emptyset)) \to \exists p \in r \forall t \in r \neg t T p$
160	159	ex	$⊢ (R We A \land R Se A \land \forall x \in A S Fr B) \to ((r \subseteq ⋃_{x \in A} B \land r \neq \emptyset) \to \exists p \in r \forall t \in r \neg t T p)$
161	160	alrimiv	$⊢ (R We A \land R Se A \land \forall x \in A S Fr B) \to \forall r ((r \subseteq ⋃_{x \in A} B \land r \neq \emptyset) \to \exists p \in r \forall t \in r \neg t T p)$
162		df-fr	$⊢ T Fr ⋃_{x \in A} B \leftrightarrow \forall r ((r \subseteq ⋃_{x \in A} B \land r \neq \emptyset) \to \exists p \in r \forall t \in r \neg t T p)$
163	161 162	sylibr	$⊢ (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 weiunfrlem2

Proof