weiunpo

Description: A partial ordering on an indexed union can be constructed from a well-ordering on its index class and a collection of partial 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	weiunpo	$⊢ (R We A \land R Se A \land \forall x \in A S Po B) \to T Po ⋃_{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		simpl1	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to R We A$
4		weso	$⊢ R We A \to R Or A$
5	3 4	syl	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to R Or A$
6		simpl2	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to R Se A$
7	1 2 3 6	weiunlem2	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} 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))$
8	7	simp1d	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to F : ⋃_{x \in A} B ⟶ A$
9		simpr1	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to p \in ⋃_{x \in A} B$
10	8 9	ffvelcdmd	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to F (p) \in A$
11		sonr	$⊢ (R Or A \land F (p) \in A) \to \neg F (p) R F (p)$
12	5 10 11	syl2anc	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to \neg F (p) R F (p)$
13		csbeq1	$⊢ s = F (p) \to ⦋ s / x ⦌ S = ⦋ F (p) / x ⦌ S$
14		csbeq1	$⊢ s = F (p) \to ⦋ s / x ⦌ B = ⦋ F (p) / x ⦌ B$
15	13 14	poeq12d	$⊢ s = F (p) \to (⦋ s / x ⦌ S Po ⦋ s / x ⦌ B \leftrightarrow ⦋ F (p) / x ⦌ S Po ⦋ F (p) / x ⦌ B)$
16		simpl3	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to \forall x \in A S Po B$
17		nfv	$⊢ Ⅎ s S Po B$
18		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ S$
19		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ B$
20	18 19	nfpo	$⊢ Ⅎ x ⦋ s / x ⦌ S Po ⦋ s / x ⦌ B$
21		csbeq1a	$⊢ x = s \to S = ⦋ s / x ⦌ S$
22		csbeq1a	$⊢ x = s \to B = ⦋ s / x ⦌ B$
23	21 22	poeq12d	$⊢ x = s \to (S Po B \leftrightarrow ⦋ s / x ⦌ S Po ⦋ s / x ⦌ B)$
24	17 20 23	cbvralw	$⊢ \forall x \in A S Po B \leftrightarrow \forall s \in A ⦋ s / x ⦌ S Po ⦋ s / x ⦌ B$
25	16 24	sylib	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to \forall s \in A ⦋ s / x ⦌ S Po ⦋ s / x ⦌ B$
26	15 25 10	rspcdva	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to ⦋ F (p) / x ⦌ S Po ⦋ F (p) / x ⦌ B$
27		id	$⊢ t = p \to t = p$
28		fveq2	$⊢ t = p \to F (t) = F (p)$
29	28	csbeq1d	$⊢ t = p \to ⦋ F (t) / x ⦌ B = ⦋ F (p) / x ⦌ B$
30	27 29	eleq12d	$⊢ t = p \to (t \in ⦋ F (t) / x ⦌ B \leftrightarrow p \in ⦋ F (p) / x ⦌ B)$
31	7	simp2d	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} 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$
32	30 31 9	rspcdva	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to p \in ⦋ F (p) / x ⦌ B$
33		poirr	$⊢ (⦋ F (p) / x ⦌ S Po ⦋ F (p) / x ⦌ B \land p \in ⦋ F (p) / x ⦌ B) \to \neg p ⦋ F (p) / x ⦌ S p$
34	26 32 33	syl2anc	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to \neg p ⦋ F (p) / x ⦌ S p$
35	34	intnand	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to \neg (F (p) = F (p) \land p ⦋ F (p) / x ⦌ S p)$
36		ioran	$⊢ \neg (F (p) R F (p) \lor (F (p) = F (p) \land p ⦋ F (p) / x ⦌ S p)) \leftrightarrow (\neg F (p) R F (p) \land \neg (F (p) = F (p) \land p ⦋ F (p) / x ⦌ S p))$
37	12 35 36	sylanbrc	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to \neg (F (p) R F (p) \lor (F (p) = F (p) \land p ⦋ F (p) / x ⦌ S p))$
38	1 2	weiunlem1	$⊢ p T p \leftrightarrow ((p \in ⋃_{x \in A} B \land p \in ⋃_{x \in A} B) \land (F (p) R F (p) \lor (F (p) = F (p) \land p ⦋ F (p) / x ⦌ S p)))$
39	38	simprbi	$⊢ p T p \to (F (p) R F (p) \lor (F (p) = F (p) \land p ⦋ F (p) / x ⦌ S p))$
40	37 39	nsyl	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to \neg p T p$
41		simpr3	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to r \in ⋃_{x \in A} B$
42	9 41	jca	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to (p \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)$
43	1 2	weiunlem1	$⊢ p T q \leftrightarrow ((p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B) \land (F (p) R F (q) \lor (F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q)))$
44	43	simprbi	$⊢ p T q \to (F (p) R F (q) \lor (F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q))$
45	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)))$
46	45	simprbi	$⊢ q T r \to (F (q) R F (r) \lor (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))$
47		simpr2	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to q \in ⋃_{x \in A} B$
48	8 47	ffvelcdmd	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to F (q) \in A$
49	8 41	ffvelcdmd	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to F (r) \in A$
50		sotr	$⊢ (R Or A \land (F (p) \in A \land F (q) \in A \land F (r) \in A)) \to ((F (p) R F (q) \land F (q) R F (r)) \to F (p) R F (r))$
51	5 10 48 49 50	syl13anc	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to ((F (p) R F (q) \land F (q) R F (r)) \to F (p) R F (r))$
52		orc	$⊢ F (p) R F (r) \to (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r))$
53	51 52	syl6	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to ((F (p) R F (q) \land F (q) R F (r)) \to (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r)))$
54		simprll	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land F (q) R F (r))) \to F (p) = F (q)$
55		simprr	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land F (q) R F (r))) \to F (q) R F (r)$
56	54 55	eqbrtrd	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land F (q) R F (r))) \to F (p) R F (r)$
57	56	orcd	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land F (q) R F (r))) \to (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r))$
58	57	ex	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to (((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land F (q) R F (r)) \to (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r)))$
59		simprl	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land (F (p) R F (q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to F (p) R F (q)$
60		simprrl	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land (F (p) R F (q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to F (q) = F (r)$
61	59 60	breqtrd	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land (F (p) R F (q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to F (p) R F (r)$
62	61	orcd	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land (F (p) R F (q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r))$
63	62	ex	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to ((F (p) R F (q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r)) \to (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r)))$
64		simprll	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to F (p) = F (q)$
65		simprrl	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to F (q) = F (r)$
66	64 65	eqtrd	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to F (p) = F (r)$
67		simprlr	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to p ⦋ F (p) / x ⦌ S q$
68		simprrr	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to q ⦋ F (q) / x ⦌ S r$
69	64	csbeq1d	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to ⦋ F (p) / x ⦌ S = ⦋ F (q) / x ⦌ S$
70	69	breqd	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to (q ⦋ F (p) / x ⦌ S r \leftrightarrow q ⦋ F (q) / x ⦌ S r)$
71	68 70	mpbird	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to q ⦋ F (p) / x ⦌ S r$
72	26	adantr	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to ⦋ F (p) / x ⦌ S Po ⦋ F (p) / x ⦌ B$
73	32	adantr	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to p \in ⦋ F (p) / x ⦌ B$
74		id	$⊢ t = q \to t = q$
75		fveq2	$⊢ t = q \to F (t) = F (q)$
76	75	csbeq1d	$⊢ t = q \to ⦋ F (t) / x ⦌ B = ⦋ F (q) / x ⦌ B$
77	74 76	eleq12d	$⊢ t = q \to (t \in ⦋ F (t) / x ⦌ B \leftrightarrow q \in ⦋ F (q) / x ⦌ B)$
78	77 31 47	rspcdva	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to q \in ⦋ F (q) / x ⦌ B$
79	78	adantr	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to q \in ⦋ F (q) / x ⦌ B$
80	64	csbeq1d	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to ⦋ F (p) / x ⦌ B = ⦋ F (q) / x ⦌ B$
81	79 80	eleqtrrd	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to q \in ⦋ F (p) / x ⦌ B$
82		id	$⊢ t = r \to t = r$
83		fveq2	$⊢ t = r \to F (t) = F (r)$
84	83	csbeq1d	$⊢ t = r \to ⦋ F (t) / x ⦌ B = ⦋ F (r) / x ⦌ B$
85	82 84	eleq12d	$⊢ t = r \to (t \in ⦋ F (t) / x ⦌ B \leftrightarrow r \in ⦋ F (r) / x ⦌ B)$
86	85 31 41	rspcdva	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to r \in ⦋ F (r) / x ⦌ B$
87	86	adantr	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to r \in ⦋ F (r) / x ⦌ B$
88	66	csbeq1d	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to ⦋ F (p) / x ⦌ B = ⦋ F (r) / x ⦌ B$
89	87 88	eleqtrrd	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to r \in ⦋ F (p) / x ⦌ B$
90		potr	$⊢ (⦋ F (p) / x ⦌ S Po ⦋ F (p) / x ⦌ B \land (p \in ⦋ F (p) / x ⦌ B \land q \in ⦋ F (p) / x ⦌ B \land r \in ⦋ F (p) / x ⦌ B)) \to ((p ⦋ F (p) / x ⦌ S q \land q ⦋ F (p) / x ⦌ S r) \to p ⦋ F (p) / x ⦌ S r)$
91	72 73 81 89 90	syl13anc	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to ((p ⦋ F (p) / x ⦌ S q \land q ⦋ F (p) / x ⦌ S r) \to p ⦋ F (p) / x ⦌ S r)$
92	67 71 91	mp2and	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to p ⦋ F (p) / x ⦌ S r$
93	66 92	jca	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r)$
94	93	olcd	$⊢ (((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \land ((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r))$
95	94	ex	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to (((F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q) \land (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r)) \to (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r)))$
96	53 58 63 95	ccased	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to (((F (p) R F (q) \lor (F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q)) \land (F (q) R F (r) \lor (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))) \to (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r)))$
97	44 46 96	syl2ani	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to ((p T q \land q T r) \to (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r)))$
98	1 2	weiunlem1	$⊢ p T r \leftrightarrow ((p \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B) \land (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r)))$
99	98	biimpri	$⊢ ((p \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B) \land (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r))) \to p T r$
100	42 97 99	syl6an	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to ((p T q \land q T r) \to p T r)$
101	40 100	jca	$⊢ ((R We A \land R Se A \land \forall x \in A S Po B) \land (p \in ⋃_{x \in A} B \land q \in ⋃_{x \in A} B \land r \in ⋃_{x \in A} B)) \to (\neg p T p \land ((p T q \land q T r) \to p T r))$
102	101	ralrimivvva	$⊢ (R We A \land R Se A \land \forall x \in A S Po B) \to \forall p \in ⋃_{x \in A} B \forall q \in ⋃_{x \in A} B \forall r \in ⋃_{x \in A} B (\neg p T p \land ((p T q \land q T r) \to p T r))$
103		df-po	$⊢ T Po ⋃_{x \in A} B \leftrightarrow \forall p \in ⋃_{x \in A} B \forall q \in ⋃_{x \in A} B \forall r \in ⋃_{x \in A} B (\neg p T p \land ((p T q \land q T r) \to p T r))$
104	102 103	sylibr	$⊢ (R We A \land R Se A \land \forall x \in A S Po B) \to T Po ⋃_{x \in A} B$

Metamath Proof Explorer

Theorem weiunpo

Proof