weiunso

Description: A strict ordering on an indexed union can be constructed from a well-ordering on its index class and a collection of strict orderings 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	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		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		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	1 2	weiunlem1	$⊢ 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)))$
11	7 8 9 10	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$
12	11	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)$
13		csbeq1	$⊢ s = F (q) \to ⦋ s / x ⦌ S = ⦋ F (q) / x ⦌ S$
14		csbeq1	$⊢ s = F (q) \to ⦋ s / x ⦌ B = ⦋ F (q) / x ⦌ B$
15	13 14	soeq12d	$⊢ s = F (q) \to (⦋ s / x ⦌ S Or ⦋ s / x ⦌ B \leftrightarrow ⦋ F (q) / x ⦌ S Or ⦋ F (q) / x ⦌ B)$
16		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$
17		nfv	$⊢ Ⅎ s S Or B$
18		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ S$
19		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ B$
20	18 19	nfso	$⊢ Ⅎ x ⦋ s / x ⦌ S Or ⦋ s / x ⦌ B$
21		csbeq1a	$⊢ x = s \to S = ⦋ s / x ⦌ S$
22		csbeq1a	$⊢ x = s \to B = ⦋ s / x ⦌ B$
23	21 22	soeq12d	$⊢ x = s \to (S Or B \leftrightarrow ⦋ s / x ⦌ S Or ⦋ s / x ⦌ B)$
24	17 20 23	cbvralw	$⊢ \forall x \in A S Or B \leftrightarrow \forall s \in A ⦋ s / x ⦌ S Or ⦋ s / x ⦌ B$
25	16 24	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$
26		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$
27		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$
28	1 2 26 27	weiunlem2	$⊢ ((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 s \in A \forall t \in ⦋ s / x ⦌ B \neg s R F (t))$
29	28	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$
30		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$
31	29 30	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$
32	31	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$
33	15 25 32	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$
34		id	$⊢ t = q \to t = q$
35		fveq2	$⊢ t = q \to F (t) = F (q)$
36	35	csbeq1d	$⊢ t = q \to ⦋ F (t) / x ⦌ B = ⦋ F (q) / x ⦌ B$
37	34 36	eleq12d	$⊢ t = q \to (t \in ⦋ F (t) / x ⦌ B \leftrightarrow q \in ⦋ F (q) / x ⦌ B)$
38	28	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$
39	38	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$
40		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$
41	37 39 40	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$
42		id	$⊢ t = r \to t = r$
43		fveq2	$⊢ t = r \to F (t) = F (r)$
44	43	csbeq1d	$⊢ t = r \to ⦋ F (t) / x ⦌ B = ⦋ F (r) / x ⦌ B$
45	42 44	eleq12d	$⊢ t = r \to (t \in ⦋ F (t) / x ⦌ B \leftrightarrow r \in ⦋ F (r) / x ⦌ B)$
46		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$
47	45 39 46	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$
48		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)$
49	48	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$
50	47 49	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$
51		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)$
52	33 41 50 51	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)$
53		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)$
54	48	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)$
55	54	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))$
56	53 55 10	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$
57	56	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)$
58		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)$
59	46	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$
60	40	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$
61		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)$
62	61	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)$
63	61	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$
64		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$
65	63 64	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$
66	62 65	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)$
67	66	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))$
68	1 2	weiunlem1	$⊢ 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)))$
69	59 60 67 68	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$
70	69	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)$
71	57 58 70	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))$
72	52 71	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)$
73		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$
74		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$
75		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))$
76	73 74 75 68	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$
77	76	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)$
78		weso	$⊢ R We A \to R Or A$
79	26 78	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$
80		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$
81	29 80	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$
82		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))$
83	79 31 81 82	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))$
84	12 72 77 83	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)$
85	6 84	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