weiunso

Description: A strict ordering on an indexed union can be constructed from a well-ordering on its index set and a collection of strict orderings on its members. (Contributed by Matthew House, 23-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		weiunso.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		weiunso.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		sopo	$⊢ S Or B \to S Po B$
4	3	ralimi	$⊢ \forall x \in A S Or B \to \forall x \in A S Po B$
5	1 2	weiunpo	$⊢ (R We A \land R Se A \land \forall x \in A S Po B) \to T Po ⋃_{x \in A} B$
6	4 5	syl3an3	$⊢ (R We A \land R Se A \land \forall x \in A S Or B) \to T Po ⋃_{x \in A} B$
7		simplrl	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) R F (r)) \to q \in ⋃_{x \in A} B$
8		simplrr	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) R F (r)) \to r \in ⋃_{x \in A} B$
9		animorrl	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) R F (r)) \to (F (q) R F (r) \lor (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))$
10		simpl	$⊢ (y = q \land z = r) \to y = q$
11	10	fveq2d	$⊢ (y = q \land z = r) \to F (y) = F (q)$
12		simpr	$⊢ (y = q \land z = r) \to z = r$
13	12	fveq2d	$⊢ (y = q \land z = r) \to F (z) = F (r)$
14	11 13	breq12d	$⊢ (y = q \land z = r) \to (F (y) R F (z) \leftrightarrow F (q) R F (r))$
15	11 13	eqeq12d	$⊢ (y = q \land z = r) \to (F (y) = F (z) \leftrightarrow F (q) = F (r))$
16	11	csbeq1d	$⊢ (y = q \land z = r) \to ⦋ F (y) / x ⦌ S = ⦋ F (q) / x ⦌ S$
17	10 16 12	breq123d	$⊢ (y = q \land z = r) \to (y ⦋ F (y) / x ⦌ S z \leftrightarrow q ⦋ F (q) / x ⦌ S r)$
18	15 17	anbi12d	$⊢ (y = q \land z = r) \to ((F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z) \leftrightarrow (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))$
19	14 18	orbi12d	$⊢ (y = q \land z = r) \to ((F (y) R F (z) \lor (F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z)) \leftrightarrow (F (q) R F (r) \lor (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r)))$
20	19 2	brab2a	$⊢ q T r \leftrightarrow ((q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B) \land (F (q) R F (r) \lor (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r)))$
21	7 8 9 20	syl21anbrc	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) R F (r)) \to q T r$
22	21	3mix1d	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) R F (r)) \to (q T r \lor q = r \lor r T q)$
23		csbeq1	$⊢ s = F (q) \to ⦋ s / x ⦌ S = ⦋ F (q) / x ⦌ S$
24		soeq1	$⊢ ⦋ s / x ⦌ S = ⦋ F (q) / x ⦌ S \to (⦋ s / x ⦌ S Or ⦋ s / x ⦌ B \leftrightarrow ⦋ F (q) / x ⦌ S Or ⦋ s / x ⦌ B)$
25	23 24	syl	$⊢ s = F (q) \to (⦋ s / x ⦌ S Or ⦋ s / x ⦌ B \leftrightarrow ⦋ F (q) / x ⦌ S Or ⦋ s / x ⦌ B)$
26		csbeq1	$⊢ s = F (q) \to ⦋ s / x ⦌ B = ⦋ F (q) / x ⦌ B$
27		soeq2	$⊢ ⦋ s / x ⦌ B = ⦋ F (q) / x ⦌ B \to (⦋ F (q) / x ⦌ S Or ⦋ s / x ⦌ B \leftrightarrow ⦋ F (q) / x ⦌ S Or ⦋ F (q) / x ⦌ B)$
28	26 27	syl	$⊢ s = F (q) \to (⦋ F (q) / x ⦌ S Or ⦋ s / x ⦌ B \leftrightarrow ⦋ F (q) / x ⦌ S Or ⦋ F (q) / x ⦌ B)$
29	25 28	bitrd	$⊢ s = F (q) \to (⦋ s / x ⦌ S Or ⦋ s / x ⦌ B \leftrightarrow ⦋ F (q) / x ⦌ S Or ⦋ F (q) / x ⦌ B)$
30		simpll3	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to \forall x \in A S Or B$
31		nfv	$⊢ Ⅎ s S Or B$
32		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ S$
33		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ B$
34	32 33	nfso	$⊢ Ⅎ x ⦋ s / x ⦌ S Or ⦋ s / x ⦌ B$
35		csbeq1a	$⊢ x = s \to S = ⦋ s / x ⦌ S$
36		soeq1	$⊢ S = ⦋ s / x ⦌ S \to (S Or B \leftrightarrow ⦋ s / x ⦌ S Or B)$
37	35 36	syl	$⊢ x = s \to (S Or B \leftrightarrow ⦋ s / x ⦌ S Or B)$
38		csbeq1a	$⊢ x = s \to B = ⦋ s / x ⦌ B$
39		soeq2	$⊢ B = ⦋ s / x ⦌ B \to (⦋ s / x ⦌ S Or B \leftrightarrow ⦋ s / x ⦌ S Or ⦋ s / x ⦌ B)$
40	38 39	syl	$⊢ x = s \to (⦋ s / x ⦌ S Or B \leftrightarrow ⦋ s / x ⦌ S Or ⦋ s / x ⦌ B)$
41	37 40	bitrd	$⊢ x = s \to (S Or B \leftrightarrow ⦋ s / x ⦌ S Or ⦋ s / x ⦌ B)$
42	31 34 41	cbvralw	$⊢ \forall x \in A S Or B \leftrightarrow \forall s \in A ⦋ s / x ⦌ S Or ⦋ s / x ⦌ B$
43	30 42	sylib	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to \forall s \in A ⦋ s / x ⦌ S Or ⦋ s / x ⦌ B$
44		simpl1	$⊢ ((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to R We A$
45		simpl2	$⊢ ((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to R Se A$
46	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)))$
47	44 45 46	syl2anc	$⊢ ((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \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)))$
48	47	simp1d	$⊢ ((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to F : ⋃_{x \in A} B ⟶ A$
49		simprl	$⊢ ((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to q \in ⋃_{x \in A} B$
50	48 49	ffvelcdmd	$⊢ ((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to F (q) \in A$
51	50	adantr	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to F (q) \in A$
52	29 43 51	rspcdva	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to ⦋ F (q) / x ⦌ S Or ⦋ F (q) / x ⦌ B$
53		id	$⊢ t = q \to t = q$
54		fveq2	$⊢ t = q \to F (t) = F (q)$
55	54	csbeq1d	$⊢ t = q \to ⦋ F (t) / x ⦌ B = ⦋ F (q) / x ⦌ B$
56	53 55	eleq12d	$⊢ t = q \to (t \in ⦋ F (t) / x ⦌ B \leftrightarrow q \in ⦋ F (q) / x ⦌ B)$
57	47	simp2d	$⊢ ((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to \forall t \in ⋃_{x \in A} B t \in ⦋ F (t) / x ⦌ B$
58	57	adantr	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to \forall t \in ⋃_{x \in A} B t \in ⦋ F (t) / x ⦌ B$
59		simplrl	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to q \in ⋃_{x \in A} B$
60	56 58 59	rspcdva	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to q \in ⦋ F (q) / x ⦌ B$
61		id	$⊢ t = r \to t = r$
62		fveq2	$⊢ t = r \to F (t) = F (r)$
63	62	csbeq1d	$⊢ t = r \to ⦋ F (t) / x ⦌ B = ⦋ F (r) / x ⦌ B$
64	61 63	eleq12d	$⊢ t = r \to (t \in ⦋ F (t) / x ⦌ B \leftrightarrow r \in ⦋ F (r) / x ⦌ B)$
65		simplrr	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to r \in ⋃_{x \in A} B$
66	64 58 65	rspcdva	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to r \in ⦋ F (r) / x ⦌ B$
67		simpr	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to F (q) = F (r)$
68	67	csbeq1d	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to ⦋ F (q) / x ⦌ B = ⦋ F (r) / x ⦌ B$
69	66 68	eleqtrrd	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to r \in ⦋ F (q) / x ⦌ B$
70		solin	$⊢ (⦋ F (q) / x ⦌ S Or ⦋ F (q) / x ⦌ B \land (q \in ⦋ F (q) / x ⦌ B \land r \in ⦋ F (q) / x ⦌ B)) \to (q ⦋ F (q) / x ⦌ S r \lor q = r \lor r ⦋ F (q) / x ⦌ S q)$
71	52 60 69 70	syl12anc	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to (q ⦋ F (q) / x ⦌ S r \lor q = r \lor r ⦋ F (q) / x ⦌ S q)$
72		simpllr	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land q ⦋ F (q) / x ⦌ S r) \to (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)$
73	67	anim1i	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land q ⦋ F (q) / x ⦌ S r) \to (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r)$
74	73	olcd	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land q ⦋ F (q) / x ⦌ S r) \to (F (q) R F (r) \lor (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))$
75	72 74 20	sylanbrc	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land q ⦋ F (q) / x ⦌ S r) \to q T r$
76	75	ex	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to (q ⦋ F (q) / x ⦌ S r \to q T r)$
77		idd	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to (q = r \to q = r)$
78	65	adantr	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land r ⦋ F (q) / x ⦌ S q) \to r \in ⋃_{x \in A} B$
79	59	adantr	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land r ⦋ F (q) / x ⦌ S q) \to q \in ⋃_{x \in A} B$
80		simplr	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land r ⦋ F (q) / x ⦌ S q) \to F (q) = F (r)$
81	80	eqcomd	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land r ⦋ F (q) / x ⦌ S q) \to F (r) = F (q)$
82	80	csbeq1d	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land r ⦋ F (q) / x ⦌ S q) \to ⦋ F (q) / x ⦌ S = ⦋ F (r) / x ⦌ S$
83		simpr	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land r ⦋ F (q) / x ⦌ S q) \to r ⦋ F (q) / x ⦌ S q$
84	82 83	breqdi	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land r ⦋ F (q) / x ⦌ S q) \to r ⦋ F (r) / x ⦌ S q$
85	81 84	jca	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land r ⦋ F (q) / x ⦌ S q) \to (F (r) = F (q) \land r ⦋ F (r) / x ⦌ S q)$
86	85	olcd	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land r ⦋ F (q) / x ⦌ S q) \to (F (r) R F (q) \lor (F (r) = F (q) \land r ⦋ F (r) / x ⦌ S q))$
87		simpl	$⊢ (y = r \land z = q) \to y = r$
88	87	fveq2d	$⊢ (y = r \land z = q) \to F (y) = F (r)$
89		simpr	$⊢ (y = r \land z = q) \to z = q$
90	89	fveq2d	$⊢ (y = r \land z = q) \to F (z) = F (q)$
91	88 90	breq12d	$⊢ (y = r \land z = q) \to (F (y) R F (z) \leftrightarrow F (r) R F (q))$
92	88 90	eqeq12d	$⊢ (y = r \land z = q) \to (F (y) = F (z) \leftrightarrow F (r) = F (q))$
93	88	csbeq1d	$⊢ (y = r \land z = q) \to ⦋ F (y) / x ⦌ S = ⦋ F (r) / x ⦌ S$
94	87 93 89	breq123d	$⊢ (y = r \land z = q) \to (y ⦋ F (y) / x ⦌ S z \leftrightarrow r ⦋ F (r) / x ⦌ S q)$
95	92 94	anbi12d	$⊢ (y = r \land z = q) \to ((F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z) \leftrightarrow (F (r) = F (q) \land r ⦋ F (r) / x ⦌ S q))$
96	91 95	orbi12d	$⊢ (y = r \land z = q) \to ((F (y) R F (z) \lor (F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z)) \leftrightarrow (F (r) R F (q) \lor (F (r) = F (q) \land r ⦋ F (r) / x ⦌ S q)))$
97	96 2	brab2a	$⊢ r T q \leftrightarrow ((r \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B) \land (F (r) R F (q) \lor (F (r) = F (q) \land r ⦋ F (r) / x ⦌ S q)))$
98	78 79 86 97	syl21anbrc	$⊢ ((((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \land r ⦋ F (q) / x ⦌ S q) \to r T q$
99	98	ex	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to (r ⦋ F (q) / x ⦌ S q \to r T q)$
100	76 77 99	3orim123d	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to ((q ⦋ F (q) / x ⦌ S r \lor q = r \lor r ⦋ F (q) / x ⦌ S q) \to (q T r \lor q = r \lor r T q))$
101	71 100	mpd	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (q) = F (r)) \to (q T r \lor q = r \lor r T q)$
102		simplrr	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (r) R F (q)) \to r \in ⋃_{x \in A} B$
103		simplrl	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (r) R F (q)) \to q \in ⋃_{x \in A} B$
104		animorrl	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (r) R F (q)) \to (F (r) R F (q) \lor (F (r) = F (q) \land r ⦋ F (r) / x ⦌ S q))$
105	102 103 104 97	syl21anbrc	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (r) R F (q)) \to r T q$
106	105	3mix3d	$⊢ (((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land F (r) R F (q)) \to (q T r \lor q = r \lor r T q)$
107		weso	$⊢ R We A \to R Or A$
108	44 107	syl	$⊢ ((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to R Or A$
109		simprr	$⊢ ((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to r \in ⋃_{x \in A} B$
110	48 109	ffvelcdmd	$⊢ ((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to F (r) \in A$
111		solin	$⊢ (R Or A \land (F (q) \in A \land F (r) \in A)) \to (F (q) R F (r) \lor F (q) = F (r) \lor F (r) R F (q))$
112	108 50 110 111	syl12anc	$⊢ ((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to (F (q) R F (r) \lor F (q) = F (r) \lor F (r) R F (q))$
113	22 101 106 112	mpjao3dan	$⊢ ((R We A \land R Se A \land \forall x \in A S Or B) \land (q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to (q T r \lor q = r \lor r T q)$
114	6 113	issod	$⊢ (R We A \land R Se A \land \forall x \in A S Or B) \to T Or ⋃_{x \in A} B$

Metamath Proof Explorer

Theorem weiunso

Proof