weiunpo

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

	Ref	Expression
Hypotheses	weiunpo.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))$
	weiunpo.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		weiunpo.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		weiunpo.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	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)))$
8	3 6 7	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 (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)))$
9	8	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$
10		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$
11	9 10	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$
12		sonr	$⊢ (R Or A \land F (p) \in A) \to \neg F (p) R F (p)$
13	5 11 12	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)$
14		csbeq1	$⊢ s = F (p) \to ⦋ s / x ⦌ S = ⦋ F (p) / x ⦌ S$
15		poeq1	$⊢ ⦋ s / x ⦌ S = ⦋ F (p) / x ⦌ S \to (⦋ s / x ⦌ S Po ⦋ s / x ⦌ B \leftrightarrow ⦋ F (p) / x ⦌ S Po ⦋ s / x ⦌ B)$
16	14 15	syl	$⊢ s = F (p) \to (⦋ s / x ⦌ S Po ⦋ s / x ⦌ B \leftrightarrow ⦋ F (p) / x ⦌ S Po ⦋ s / x ⦌ B)$
17		csbeq1	$⊢ s = F (p) \to ⦋ s / x ⦌ B = ⦋ F (p) / x ⦌ B$
18		poeq2	$⊢ ⦋ s / x ⦌ B = ⦋ F (p) / x ⦌ B \to (⦋ F (p) / x ⦌ S Po ⦋ s / x ⦌ B \leftrightarrow ⦋ F (p) / x ⦌ S Po ⦋ F (p) / x ⦌ B)$
19	17 18	syl	$⊢ s = F (p) \to (⦋ F (p) / x ⦌ S Po ⦋ s / x ⦌ B \leftrightarrow ⦋ F (p) / x ⦌ S Po ⦋ F (p) / x ⦌ B)$
20	16 19	bitrd	$⊢ s = F (p) \to (⦋ s / x ⦌ S Po ⦋ s / x ⦌ B \leftrightarrow ⦋ F (p) / x ⦌ S Po ⦋ F (p) / x ⦌ B)$
21		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$
22		nfv	$⊢ Ⅎ s S Po B$
23		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ S$
24		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ s / x ⦌ B$
25	23 24	nfpo	$⊢ Ⅎ x ⦋ s / x ⦌ S Po ⦋ s / x ⦌ B$
26		csbeq1a	$⊢ x = s \to S = ⦋ s / x ⦌ S$
27		poeq1	$⊢ S = ⦋ s / x ⦌ S \to (S Po B \leftrightarrow ⦋ s / x ⦌ S Po B)$
28	26 27	syl	$⊢ x = s \to (S Po B \leftrightarrow ⦋ s / x ⦌ S Po B)$
29		csbeq1a	$⊢ x = s \to B = ⦋ s / x ⦌ B$
30		poeq2	$⊢ B = ⦋ s / x ⦌ B \to (⦋ s / x ⦌ S Po B \leftrightarrow ⦋ s / x ⦌ S Po ⦋ s / x ⦌ B)$
31	29 30	syl	$⊢ x = s \to (⦋ s / x ⦌ S Po B \leftrightarrow ⦋ s / x ⦌ S Po ⦋ s / x ⦌ B)$
32	28 31	bitrd	$⊢ x = s \to (S Po B \leftrightarrow ⦋ s / x ⦌ S Po ⦋ s / x ⦌ B)$
33	22 25 32	cbvralw	$⊢ \forall x \in A S Po B \leftrightarrow \forall s \in A ⦋ s / x ⦌ S Po ⦋ s / x ⦌ B$
34	21 33	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$
35	20 34 11	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$
36		id	$⊢ t = p \to t = p$
37		fveq2	$⊢ t = p \to F (t) = F (p)$
38	37	csbeq1d	$⊢ t = p \to ⦋ F (t) / x ⦌ B = ⦋ F (p) / x ⦌ B$
39	36 38	eleq12d	$⊢ t = p \to (t \in ⦋ F (t) / x ⦌ B \leftrightarrow p \in ⦋ F (p) / x ⦌ B)$
40	8	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$
41	39 40 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 p \in ⦋ F (p) / x ⦌ B$
42		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$
43	35 41 42	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$
44	43	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)$
45		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))$
46	13 44 45	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))$
47		simpl	$⊢ (y = p \land z = p) \to y = p$
48	47	fveq2d	$⊢ (y = p \land z = p) \to F (y) = F (p)$
49		simpr	$⊢ (y = p \land z = p) \to z = p$
50	49	fveq2d	$⊢ (y = p \land z = p) \to F (z) = F (p)$
51	48 50	breq12d	$⊢ (y = p \land z = p) \to (F (y) R F (z) \leftrightarrow F (p) R F (p))$
52	48 50	eqeq12d	$⊢ (y = p \land z = p) \to (F (y) = F (z) \leftrightarrow F (p) = F (p))$
53	48	csbeq1d	$⊢ (y = p \land z = p) \to ⦋ F (y) / x ⦌ S = ⦋ F (p) / x ⦌ S$
54	47 53 49	breq123d	$⊢ (y = p \land z = p) \to (y ⦋ F (y) / x ⦌ S z \leftrightarrow p ⦋ F (p) / x ⦌ S p)$
55	52 54	anbi12d	$⊢ (y = p \land z = p) \to ((F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z) \leftrightarrow (F (p) = F (p) \land p ⦋ F (p) / x ⦌ S p))$
56	51 55	orbi12d	$⊢ (y = p \land z = p) \to ((F (y) R F (z) \lor (F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z)) \leftrightarrow (F (p) R F (p) \lor (F (p) = F (p) \land p ⦋ F (p) / x ⦌ S p)))$
57	56 2	brab2a	$⊢ 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)))$
58	57	simprbi	$⊢ p T p \to (F (p) R F (p) \lor (F (p) = F (p) \land p ⦋ F (p) / x ⦌ S p))$
59	46 58	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$
60		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$
61	10 60	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)$
62		simpl	$⊢ (y = p \land z = q) \to y = p$
63	62	fveq2d	$⊢ (y = p \land z = q) \to F (y) = F (p)$
64		simpr	$⊢ (y = p \land z = q) \to z = q$
65	64	fveq2d	$⊢ (y = p \land z = q) \to F (z) = F (q)$
66	63 65	breq12d	$⊢ (y = p \land z = q) \to (F (y) R F (z) \leftrightarrow F (p) R F (q))$
67	63 65	eqeq12d	$⊢ (y = p \land z = q) \to (F (y) = F (z) \leftrightarrow F (p) = F (q))$
68	63	csbeq1d	$⊢ (y = p \land z = q) \to ⦋ F (y) / x ⦌ S = ⦋ F (p) / x ⦌ S$
69	62 68 64	breq123d	$⊢ (y = p \land z = q) \to (y ⦋ F (y) / x ⦌ S z \leftrightarrow p ⦋ F (p) / x ⦌ S q)$
70	67 69	anbi12d	$⊢ (y = p \land z = q) \to ((F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z) \leftrightarrow (F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q))$
71	66 70	orbi12d	$⊢ (y = p \land z = q) \to ((F (y) R F (z) \lor (F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z)) \leftrightarrow (F (p) R F (q) \lor (F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q)))$
72	71 2	brab2a	$⊢ 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)))$
73	72	simprbi	$⊢ p T q \to (F (p) R F (q) \lor (F (p) = F (q) \land p ⦋ F (p) / x ⦌ S q))$
74		simpl	$⊢ (y = q \land z = r) \to y = q$
75	74	fveq2d	$⊢ (y = q \land z = r) \to F (y) = F (q)$
76		simpr	$⊢ (y = q \land z = r) \to z = r$
77	76	fveq2d	$⊢ (y = q \land z = r) \to F (z) = F (r)$
78	75 77	breq12d	$⊢ (y = q \land z = r) \to (F (y) R F (z) \leftrightarrow F (q) R F (r))$
79	75 77	eqeq12d	$⊢ (y = q \land z = r) \to (F (y) = F (z) \leftrightarrow F (q) = F (r))$
80	75	csbeq1d	$⊢ (y = q \land z = r) \to ⦋ F (y) / x ⦌ S = ⦋ F (q) / x ⦌ S$
81	74 80 76	breq123d	$⊢ (y = q \land z = r) \to (y ⦋ F (y) / x ⦌ S z \leftrightarrow q ⦋ F (q) / x ⦌ S r)$
82	79 81	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))$
83	78 82	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)))$
84	83 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)))$
85	84	simprbi	$⊢ q T r \to (F (q) R F (r) \lor (F (q) = F (r) \land q ⦋ F (q) / x ⦌ S r))$
86		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$
87	9 86	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$
88	9 60	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$
89		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))$
90	5 11 87 88 89	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))$
91	90	imp	$⊢ (((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) R F (r))) \to F (p) R F (r)$
92	91	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) R F (r))) \to (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r))$
93	92	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) R F (r)) \to (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r)))$
94		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)$
95		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)$
96	94 95	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)$
97	96	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))$
98	97	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)))$
99		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)$
100		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)$
101	99 100	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)$
102	101	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))$
103	102	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)))$
104		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)$
105		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)$
106	104 105	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)$
107		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$
108		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$
109	104	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$
110	109	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)$
111	108 110	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$
112	35	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$
113	41	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$
114		id	$⊢ t = q \to t = q$
115		fveq2	$⊢ t = q \to F (t) = F (q)$
116	115	csbeq1d	$⊢ t = q \to ⦋ F (t) / x ⦌ B = ⦋ F (q) / x ⦌ B$
117	114 116	eleq12d	$⊢ t = q \to (t \in ⦋ F (t) / x ⦌ B \leftrightarrow q \in ⦋ F (q) / x ⦌ B)$
118	117 40 86	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$
119	118	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$
120	104	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$
121	119 120	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$
122		id	$⊢ t = r \to t = r$
123		fveq2	$⊢ t = r \to F (t) = F (r)$
124	123	csbeq1d	$⊢ t = r \to ⦋ F (t) / x ⦌ B = ⦋ F (r) / x ⦌ B$
125	122 124	eleq12d	$⊢ t = r \to (t \in ⦋ F (t) / x ⦌ B \leftrightarrow r \in ⦋ F (r) / x ⦌ B)$
126	125 40 60	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$
127	126	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$
128	106	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$
129	127 128	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$
130		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)$
131	112 113 121 129 130	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)$
132	107 111 131	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$
133	106 132	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)$
134	133	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))$
135	134	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)))$
136	93 98 103 135	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)))$
137	73 85 136	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)))$
138		simpl	$⊢ (y = p \land z = r) \to y = p$
139	138	fveq2d	$⊢ (y = p \land z = r) \to F (y) = F (p)$
140		simpr	$⊢ (y = p \land z = r) \to z = r$
141	140	fveq2d	$⊢ (y = p \land z = r) \to F (z) = F (r)$
142	139 141	breq12d	$⊢ (y = p \land z = r) \to (F (y) R F (z) \leftrightarrow F (p) R F (r))$
143	139 141	eqeq12d	$⊢ (y = p \land z = r) \to (F (y) = F (z) \leftrightarrow F (p) = F (r))$
144	139	csbeq1d	$⊢ (y = p \land z = r) \to ⦋ F (y) / x ⦌ S = ⦋ F (p) / x ⦌ S$
145	138 144 140	breq123d	$⊢ (y = p \land z = r) \to (y ⦋ F (y) / x ⦌ S z \leftrightarrow p ⦋ F (p) / x ⦌ S r)$
146	143 145	anbi12d	$⊢ (y = p \land z = r) \to ((F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z) \leftrightarrow (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r))$
147	142 146	orbi12d	$⊢ (y = p \land z = r) \to ((F (y) R F (z) \lor (F (y) = F (z) \land y ⦋ F (y) / x ⦌ S z)) \leftrightarrow (F (p) R F (r) \lor (F (p) = F (r) \land p ⦋ F (p) / x ⦌ S r)))$
148	147 2	brab2a	$⊢ 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)))$
149	148	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$
150	61 137 149	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)$
151	59 150	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))$
152	151	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))$
153		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))$
154	152 153	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