weiunfr

Description: A well-founded relation on an indexed union can be constructed from a well-ordering on its index class and a collection of well-founded relations on its members. (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	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		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		csbeq1	$⊢ s = (ι p \in F [r] \| \forall q \in F [r] \neg q R p) \to ⦋ s / x ⦌ S = ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S$
4		csbeq1	$⊢ s = (ι p \in F [r] \| \forall q \in F [r] \neg q R p) \to ⦋ s / x ⦌ B = ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B$
5	3 4	freq12d	$⊢ s = (ι p \in F [r] \| \forall q \in F [r] \neg q R p) \to (⦋ s / x ⦌ S Fr ⦋ s / x ⦌ B \leftrightarrow ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S Fr ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B)$
6		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$
7		nfv	$⊢ Ⅎ s S Fr B$
8		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ S$
9		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ B$
10	8 9	nffr	$⊢ Ⅎ x ⦋ s / x ⦌ S Fr ⦋ s / x ⦌ B$
11		csbeq1a	$⊢ x = s \to S = ⦋ s / x ⦌ S$
12		csbeq1a	$⊢ x = s \to B = ⦋ s / x ⦌ B$
13	11 12	freq12d	$⊢ x = s \to (S Fr B \leftrightarrow ⦋ s / x ⦌ S Fr ⦋ s / x ⦌ B)$
14	7 10 13	cbvralw	$⊢ \forall x \in A S Fr B \leftrightarrow \forall s \in A ⦋ s / x ⦌ S Fr ⦋ s / x ⦌ B$
15	6 14	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)) \to \forall s \in A ⦋ s / x ⦌ S Fr ⦋ s / x ⦌ B$
16		simpl1	$⊢ ((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 We A$
17		simpl2	$⊢ ((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 Se A$
18	1 2 16 17	weiunlem2	$⊢ ((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 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))$
19	18	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$
20	19	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$
21		eqid	$⊢ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p)$
22		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)) \to r \subseteq ⋃_{x \in A} B$
23		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)) \to r \neq \emptyset$
24	1 2 16 17 21 22 23	weiunfrlem	$⊢ ((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 ((ι p \in F [r] \| \forall q \in F [r] \neg q R p) \in F [r] \land \forall t \in r \neg F (t) R (ι p \in F [r] \| \forall q \in F [r] \neg q R p) \land \forall t \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p))$
25	24	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 (ι p \in F [r] \| \forall q \in F [r] \neg q R p) \in F [r]$
26	20 25	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 (ι p \in F [r] \| \forall q \in F [r] \neg q R p) \in A$
27	5 15 26	rspcdva	$⊢ ((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 ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S Fr ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B$
28		inss2	$⊢ r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B \subseteq ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B$
29	28	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 ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B \subseteq ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B$
30		vex	$⊢ r \in V$
31	30	inex1	$⊢ r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B \in V$
32	31	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 ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B \in V$
33	19	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$
34		fvelima	$⊢ (Fun F \land (ι p \in F [r] \| \forall q \in F [r] \neg q R p) \in F [r]) \to \exists t \in r F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p)$
35	33 25 34	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 t \in r F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p)$
36		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 (t \in r \land F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p))) \to t \in r$
37		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 (t \in r \land F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p))) \to r \subseteq ⋃_{x \in A} B$
38	37 36	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 (t \in r \land F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p))) \to t \in ⋃_{x \in A} B$
39	18	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 t \in ⋃_{x \in A} B t \in ⦋ F (t) / x ⦌ B$
40	39	r19.21bi	$⊢ (((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 t \in ⋃_{x \in A} B) \to t \in ⦋ F (t) / x ⦌ B$
41	38 40	syldan	$⊢ (((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 (t \in r \land F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p))) \to t \in ⦋ F (t) / x ⦌ B$
42		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 (t \in r \land F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p))) \to F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p)$
43	42	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 (t \in r \land F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p))) \to ⦋ F (t) / x ⦌ B = ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B$
44	41 43	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 (t \in r \land F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p))) \to t \in ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B$
45	36 44	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 (t \in r \land F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p))) \to t \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B)$
46	45	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 (t \in r \land F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p))) \to r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B \neq \emptyset$
47	35 46	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 ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B \neq \emptyset$
48	27 29 32 47	frd	$⊢ ((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 n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n$
49		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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \to n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B)$
50	49	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \to n \in r$
51		fveq2	$⊢ t = o \to F (t) = F (o)$
52	51	breq1d	$⊢ t = o \to (F (t) R (ι p \in F [r] \| \forall q \in F [r] \neg q R p) \leftrightarrow F (o) R (ι p \in F [r] \| \forall q \in F [r] \neg q R p))$
53	52	notbid	$⊢ t = o \to (\neg F (t) R (ι p \in F [r] \| \forall q \in F [r] \neg q R p) \leftrightarrow \neg F (o) R (ι p \in F [r] \| \forall q \in F [r] \neg q R p))$
54	24	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to ((ι p \in F [r] \| \forall q \in F [r] \neg q R p) \in F [r] \land \forall t \in r \neg F (t) R (ι p \in F [r] \| \forall q \in F [r] \neg q R p) \land \forall t \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p))$
55	54	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)) \land (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to \forall t \in r \neg F (t) R (ι p \in F [r] \| \forall q \in F [r] \neg q R p)$
56		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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to o \in r$
57	53 55 56	rspcdva	$⊢ ((((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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to \neg F (o) R (ι p \in F [r] \| \forall q \in F [r] \neg q R p)$
58		fveqeq2	$⊢ t = n \to (F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p) \leftrightarrow F (n) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p))$
59	54	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to \forall t \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) F (t) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p)$
60		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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B)$
61	58 59 60	rspcdva	$⊢ ((((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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to F (n) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p)$
62	61	breq2d	$⊢ ((((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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to (F (o) R F (n) \leftrightarrow F (o) R (ι p \in F [r] \| \forall q \in F [r] \neg q R p))$
63	57 62	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to \neg F (o) R F (n)$
64		breq1	$⊢ m = o \to (m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n \leftrightarrow o ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)$
65	64	notbid	$⊢ m = o \to (\neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n \leftrightarrow \neg o ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)$
66		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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \to \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n$
67	66	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n$
68		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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to o \in r$
69		id	$⊢ t = o \to t = o$
70	51	csbeq1d	$⊢ t = o \to ⦋ F (t) / x ⦌ B = ⦋ F (o) / x ⦌ B$
71	69 70	eleq12d	$⊢ t = o \to (t \in ⦋ F (t) / x ⦌ B \leftrightarrow o \in ⦋ F (o) / x ⦌ B)$
72	39	ad3antrrr	$⊢ (((((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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to \forall t \in ⋃_{x \in A} B t \in ⦋ F (t) / x ⦌ B$
73	22	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to r \subseteq ⋃_{x \in A} B$
74	73 56	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to o \in ⋃_{x \in A} B$
75	74	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to o \in ⋃_{x \in A} B$
76	71 72 75	rspcdva	$⊢ (((((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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to o \in ⦋ F (o) / x ⦌ B$
77		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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to F (o) = F (n)$
78	61	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to F (n) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p)$
79	77 78	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to F (o) = (ι p \in F [r] \| \forall q \in F [r] \neg q R p)$
80	79	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to ⦋ F (o) / x ⦌ B = ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B$
81	76 80	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to o \in ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B$
82	68 81	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to o \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B)$
83	65 67 82	rspcdva	$⊢ (((((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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to \neg o ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n$
84	79	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to ⦋ F (o) / x ⦌ S = ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S$
85	84	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to (o ⦋ F (o) / x ⦌ S n \leftrightarrow o ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)$
86	83 85	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \land F (o) = F (n)) \to \neg o ⦋ F (o) / x ⦌ S n$
87	86	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to (F (o) = F (n) \to \neg o ⦋ F (o) / x ⦌ S n)$
88		imnan	$⊢ (F (o) = F (n) \to \neg o ⦋ F (o) / x ⦌ S n) \leftrightarrow \neg (F (o) = F (n) \land o ⦋ F (o) / x ⦌ S n)$
89	87 88	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to \neg (F (o) = F (n) \land o ⦋ F (o) / x ⦌ S n)$
90		pm4.56	$⊢ (\neg F (o) R F (n) \land \neg (F (o) = F (n) \land o ⦋ F (o) / x ⦌ S n)) \leftrightarrow \neg (F (o) R F (n) \lor (F (o) = F (n) \land o ⦋ F (o) / x ⦌ S n))$
91	90	biimpi	$⊢ (\neg F (o) R F (n) \land \neg (F (o) = F (n) \land o ⦋ F (o) / x ⦌ S n)) \to \neg (F (o) R F (n) \lor (F (o) = F (n) \land o ⦋ F (o) / x ⦌ S n))$
92	63 89 91	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to \neg (F (o) R F (n) \lor (F (o) = F (n) \land o ⦋ F (o) / x ⦌ S n))$
93	92	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to \neg ((o \in ⋃_{x \in A} B \land n \in ⋃_{x \in A} B) \land (F (o) R F (n) \lor (F (o) = F (n) \land o ⦋ F (o) / x ⦌ S n)))$
94	1 2	weiunlem1	$⊢ o T n \leftrightarrow ((o \in ⋃_{x \in A} B \land n \in ⋃_{x \in A} B) \land (F (o) R F (n) \lor (F (o) = F (n) \land o ⦋ F (o) / x ⦌ S n)))$
95	93 94	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \land o \in r) \to \neg o T n$
96	95	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 (n \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \land \forall m \in (r \cap ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ B) \neg m ⦋ (ι p \in F [r] \| \forall q \in F [r] \neg q R p) / x ⦌ S n)) \to \forall o \in r \neg o T n$
97	48 50 96	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 n \in r \forall o \in r \neg o T n$
98	97	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 n \in r \forall o \in r \neg o T n)$
99	98	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 n \in r \forall o \in r \neg o T n)$
100		df-fr	$⊢ T Fr ⋃_{x \in A} B \leftrightarrow \forall r ((r \subseteq ⋃_{x \in A} B \land r \neq \emptyset) \to \exists n \in r \forall o \in r \neg o T n)$
101	99 100	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 weiunfr

Proof