ordtbas2

	Ref	Expression
Hypotheses	ordtval.1	$⊢ X = dom R$
	ordtval.2	$⊢ A = ran (x \in X ⟼ \{y \in X \| \neg y R x\})$
	ordtval.3	$⊢ B = ran (x \in X ⟼ \{y \in X \| \neg x R y\})$
	ordtval.4	$⊢ C = ran (a \in X, b \in X ⟼ \{y \in X \| (\neg y R a \land \neg b R y)\})$
Assertion	ordtbas2	$⊢ R \in TosetRel \to fi (A \cup B) = (A \cup B) \cup C$

Proof

Step	Hyp	Ref	Expression
1		ordtval.1	$⊢ X = dom R$
2		ordtval.2	$⊢ A = ran (x \in X ⟼ \{y \in X \| \neg y R x\})$
3		ordtval.3	$⊢ B = ran (x \in X ⟼ \{y \in X \| \neg x R y\})$
4		ordtval.4	$⊢ C = ran (a \in X, b \in X ⟼ \{y \in X \| (\neg y R a \land \neg b R y)\})$
5		ssun1	$⊢ A \subseteq A \cup B$
6		ssun2	$⊢ A \cup B \subseteq \{X\} \cup (A \cup B)$
7	1 2 3	ordtuni	$⊢ R \in TosetRel \to X = ⋃ (\{X\} \cup (A \cup B))$
8		dmexg	$⊢ R \in TosetRel \to dom R \in V$
9	1 8	eqeltrid	$⊢ R \in TosetRel \to X \in V$
10	7 9	eqeltrrd	$⊢ R \in TosetRel \to ⋃ (\{X\} \cup (A \cup B)) \in V$
11		uniexb	$⊢ \{X\} \cup (A \cup B) \in V \leftrightarrow ⋃ (\{X\} \cup (A \cup B)) \in V$
12	10 11	sylibr	$⊢ R \in TosetRel \to \{X\} \cup (A \cup B) \in V$
13		ssexg	$⊢ (A \cup B \subseteq \{X\} \cup (A \cup B) \land \{X\} \cup (A \cup B) \in V) \to A \cup B \in V$
14	6 12 13	sylancr	$⊢ R \in TosetRel \to A \cup B \in V$
15		ssexg	$⊢ (A \subseteq A \cup B \land A \cup B \in V) \to A \in V$
16	5 14 15	sylancr	$⊢ R \in TosetRel \to A \in V$
17		ssun2	$⊢ B \subseteq A \cup B$
18		ssexg	$⊢ (B \subseteq A \cup B \land A \cup B \in V) \to B \in V$
19	17 14 18	sylancr	$⊢ R \in TosetRel \to B \in V$
20		elfiun	$⊢ (A \in V \land B \in V) \to (z \in fi (A \cup B) \leftrightarrow (z \in fi (A) \lor z \in fi (B) \lor \exists m \in fi (A) \exists n \in fi (B) z = m \cap n))$
21	16 19 20	syl2anc	$⊢ R \in TosetRel \to (z \in fi (A \cup B) \leftrightarrow (z \in fi (A) \lor z \in fi (B) \lor \exists m \in fi (A) \exists n \in fi (B) z = m \cap n))$
22	1 2	ordtbaslem	$⊢ R \in TosetRel \to fi (A) = A$
23	22 5	eqsstrdi	$⊢ R \in TosetRel \to fi (A) \subseteq A \cup B$
24		ssun1	$⊢ A \cup B \subseteq (A \cup B) \cup C$
25	23 24	sstrdi	$⊢ R \in TosetRel \to fi (A) \subseteq (A \cup B) \cup C$
26	25	sseld	$⊢ R \in TosetRel \to (z \in fi (A) \to z \in ((A \cup B) \cup C))$
27		cnvtsr	$⊢ R \in TosetRel \to R^{-1} \in TosetRel$
28		df-rn	$⊢ ran R = dom R^{-1}$
29		eqid	$⊢ ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\}) = ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\})$
30	28 29	ordtbaslem	$⊢ R^{-1} \in TosetRel \to fi (ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\})) = ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\})$
31	27 30	syl	$⊢ R \in TosetRel \to fi (ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\})) = ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\})$
32		tsrps	$⊢ R \in TosetRel \to R \in PosetRel$
33	1	psrn	$⊢ R \in PosetRel \to X = ran R$
34	32 33	syl	$⊢ R \in TosetRel \to X = ran R$
35		vex	$⊢ y \in V$
36		vex	$⊢ x \in V$
37	35 36	brcnv	$⊢ y R^{-1} x \leftrightarrow x R y$
38	37	bicomi	$⊢ x R y \leftrightarrow y R^{-1} x$
39	38	notbii	$⊢ \neg x R y \leftrightarrow \neg y R^{-1} x$
40	39	a1i	$⊢ R \in TosetRel \to (\neg x R y \leftrightarrow \neg y R^{-1} x)$
41	34 40	rabeqbidv	$⊢ R \in TosetRel \to \{y \in X \| \neg x R y\} = \{y \in ran R \| \neg y R^{-1} x\}$
42	34 41	mpteq12dv	$⊢ R \in TosetRel \to (x \in X ⟼ \{y \in X \| \neg x R y\}) = (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\})$
43	42	rneqd	$⊢ R \in TosetRel \to ran (x \in X ⟼ \{y \in X \| \neg x R y\}) = ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\})$
44	3 43	syl5eq	$⊢ R \in TosetRel \to B = ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\})$
45	44	fveq2d	$⊢ R \in TosetRel \to fi (B) = fi (ran (x \in ran R ⟼ \{y \in ran R \| \neg y R^{-1} x\}))$
46	31 45 44	3eqtr4d	$⊢ R \in TosetRel \to fi (B) = B$
47	46 17	eqsstrdi	$⊢ R \in TosetRel \to fi (B) \subseteq A \cup B$
48	47 24	sstrdi	$⊢ R \in TosetRel \to fi (B) \subseteq (A \cup B) \cup C$
49	48	sseld	$⊢ R \in TosetRel \to (z \in fi (B) \to z \in ((A \cup B) \cup C))$
50		ssun2	$⊢ C \subseteq (A \cup B) \cup C$
51	22 2	eqtrdi	$⊢ R \in TosetRel \to fi (A) = ran (x \in X ⟼ \{y \in X \| \neg y R x\})$
52	51	eleq2d	$⊢ R \in TosetRel \to (m \in fi (A) \leftrightarrow m \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}))$
53		breq2	$⊢ x = a \to (y R x \leftrightarrow y R a)$
54	53	notbid	$⊢ x = a \to (\neg y R x \leftrightarrow \neg y R a)$
55	54	rabbidv	$⊢ x = a \to \{y \in X \| \neg y R x\} = \{y \in X \| \neg y R a\}$
56	55	cbvmptv	$⊢ (x \in X ⟼ \{y \in X \| \neg y R x\}) = (a \in X ⟼ \{y \in X \| \neg y R a\})$
57	56	elrnmpt	$⊢ m \in V \to (m \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) \leftrightarrow \exists a \in X m = \{y \in X \| \neg y R a\})$
58	57	elv	$⊢ m \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) \leftrightarrow \exists a \in X m = \{y \in X \| \neg y R a\}$
59	52 58	bitrdi	$⊢ R \in TosetRel \to (m \in fi (A) \leftrightarrow \exists a \in X m = \{y \in X \| \neg y R a\})$
60	46 3	eqtrdi	$⊢ R \in TosetRel \to fi (B) = ran (x \in X ⟼ \{y \in X \| \neg x R y\})$
61	60	eleq2d	$⊢ R \in TosetRel \to (n \in fi (B) \leftrightarrow n \in ran (x \in X ⟼ \{y \in X \| \neg x R y\}))$
62		breq1	$⊢ x = b \to (x R y \leftrightarrow b R y)$
63	62	notbid	$⊢ x = b \to (\neg x R y \leftrightarrow \neg b R y)$
64	63	rabbidv	$⊢ x = b \to \{y \in X \| \neg x R y\} = \{y \in X \| \neg b R y\}$
65	64	cbvmptv	$⊢ (x \in X ⟼ \{y \in X \| \neg x R y\}) = (b \in X ⟼ \{y \in X \| \neg b R y\})$
66	65	elrnmpt	$⊢ n \in V \to (n \in ran (x \in X ⟼ \{y \in X \| \neg x R y\}) \leftrightarrow \exists b \in X n = \{y \in X \| \neg b R y\})$
67	66	elv	$⊢ n \in ran (x \in X ⟼ \{y \in X \| \neg x R y\}) \leftrightarrow \exists b \in X n = \{y \in X \| \neg b R y\}$
68	61 67	bitrdi	$⊢ R \in TosetRel \to (n \in fi (B) \leftrightarrow \exists b \in X n = \{y \in X \| \neg b R y\})$
69	59 68	anbi12d	$⊢ R \in TosetRel \to ((m \in fi (A) \land n \in fi (B)) \leftrightarrow (\exists a \in X m = \{y \in X \| \neg y R a\} \land \exists b \in X n = \{y \in X \| \neg b R y\}))$
70		reeanv	$⊢ \exists a \in X \exists b \in X (m = \{y \in X \| \neg y R a\} \land n = \{y \in X \| \neg b R y\}) \leftrightarrow (\exists a \in X m = \{y \in X \| \neg y R a\} \land \exists b \in X n = \{y \in X \| \neg b R y\})$
71		ineq12	$⊢ (m = \{y \in X \| \neg y R a\} \land n = \{y \in X \| \neg b R y\}) \to m \cap n = \{y \in X \| \neg y R a\} \cap \{y \in X \| \neg b R y\}$
72		inrab	$⊢ \{y \in X \| \neg y R a\} \cap \{y \in X \| \neg b R y\} = \{y \in X \| (\neg y R a \land \neg b R y)\}$
73	71 72	eqtrdi	$⊢ (m = \{y \in X \| \neg y R a\} \land n = \{y \in X \| \neg b R y\}) \to m \cap n = \{y \in X \| (\neg y R a \land \neg b R y)\}$
74	73	reximi	$⊢ \exists b \in X (m = \{y \in X \| \neg y R a\} \land n = \{y \in X \| \neg b R y\}) \to \exists b \in X m \cap n = \{y \in X \| (\neg y R a \land \neg b R y)\}$
75	74	reximi	$⊢ \exists a \in X \exists b \in X (m = \{y \in X \| \neg y R a\} \land n = \{y \in X \| \neg b R y\}) \to \exists a \in X \exists b \in X m \cap n = \{y \in X \| (\neg y R a \land \neg b R y)\}$
76	70 75	sylbir	$⊢ (\exists a \in X m = \{y \in X \| \neg y R a\} \land \exists b \in X n = \{y \in X \| \neg b R y\}) \to \exists a \in X \exists b \in X m \cap n = \{y \in X \| (\neg y R a \land \neg b R y)\}$
77	69 76	syl6bi	$⊢ R \in TosetRel \to ((m \in fi (A) \land n \in fi (B)) \to \exists a \in X \exists b \in X m \cap n = \{y \in X \| (\neg y R a \land \neg b R y)\})$
78	77	imp	$⊢ (R \in TosetRel \land (m \in fi (A) \land n \in fi (B))) \to \exists a \in X \exists b \in X m \cap n = \{y \in X \| (\neg y R a \land \neg b R y)\}$
79		vex	$⊢ m \in V$
80	79	inex1	$⊢ m \cap n \in V$
81		eqid	$⊢ (a \in X, b \in X ⟼ \{y \in X \| (\neg y R a \land \neg b R y)\}) = (a \in X, b \in X ⟼ \{y \in X \| (\neg y R a \land \neg b R y)\})$
82	81	elrnmpog	$⊢ m \cap n \in V \to (m \cap n \in ran (a \in X, b \in X ⟼ \{y \in X \| (\neg y R a \land \neg b R y)\}) \leftrightarrow \exists a \in X \exists b \in X m \cap n = \{y \in X \| (\neg y R a \land \neg b R y)\})$
83	80 82	ax-mp	$⊢ m \cap n \in ran (a \in X, b \in X ⟼ \{y \in X \| (\neg y R a \land \neg b R y)\}) \leftrightarrow \exists a \in X \exists b \in X m \cap n = \{y \in X \| (\neg y R a \land \neg b R y)\}$
84	78 83	sylibr	$⊢ (R \in TosetRel \land (m \in fi (A) \land n \in fi (B))) \to m \cap n \in ran (a \in X, b \in X ⟼ \{y \in X \| (\neg y R a \land \neg b R y)\})$
85	84 4	eleqtrrdi	$⊢ (R \in TosetRel \land (m \in fi (A) \land n \in fi (B))) \to m \cap n \in C$
86	50 85	sselid	$⊢ (R \in TosetRel \land (m \in fi (A) \land n \in fi (B))) \to m \cap n \in ((A \cup B) \cup C)$
87		eleq1	$⊢ z = m \cap n \to (z \in ((A \cup B) \cup C) \leftrightarrow m \cap n \in ((A \cup B) \cup C))$
88	86 87	syl5ibrcom	$⊢ (R \in TosetRel \land (m \in fi (A) \land n \in fi (B))) \to (z = m \cap n \to z \in ((A \cup B) \cup C))$
89	88	rexlimdvva	$⊢ R \in TosetRel \to (\exists m \in fi (A) \exists n \in fi (B) z = m \cap n \to z \in ((A \cup B) \cup C))$
90	26 49 89	3jaod	$⊢ R \in TosetRel \to ((z \in fi (A) \lor z \in fi (B) \lor \exists m \in fi (A) \exists n \in fi (B) z = m \cap n) \to z \in ((A \cup B) \cup C))$
91	21 90	sylbid	$⊢ R \in TosetRel \to (z \in fi (A \cup B) \to z \in ((A \cup B) \cup C))$
92	91	ssrdv	$⊢ R \in TosetRel \to fi (A \cup B) \subseteq (A \cup B) \cup C$
93		ssfii	$⊢ A \cup B \in V \to A \cup B \subseteq fi (A \cup B)$
94	14 93	syl	$⊢ R \in TosetRel \to A \cup B \subseteq fi (A \cup B)$
95	94	adantr	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to A \cup B \subseteq fi (A \cup B)$
96		simprl	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to a \in X$
97		eqidd	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg y R a\} = \{y \in X \| \neg y R a\}$
98	55	rspceeqv	$⊢ (a \in X \land \{y \in X \| \neg y R a\} = \{y \in X \| \neg y R a\}) \to \exists x \in X \{y \in X \| \neg y R a\} = \{y \in X \| \neg y R x\}$
99	96 97 98	syl2anc	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \exists x \in X \{y \in X \| \neg y R a\} = \{y \in X \| \neg y R x\}$
100	9	adantr	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to X \in V$
101		rabexg	$⊢ X \in V \to \{y \in X \| \neg y R a\} \in V$
102		eqid	$⊢ (x \in X ⟼ \{y \in X \| \neg y R x\}) = (x \in X ⟼ \{y \in X \| \neg y R x\})$
103	102	elrnmpt	$⊢ \{y \in X \| \neg y R a\} \in V \to (\{y \in X \| \neg y R a\} \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) \leftrightarrow \exists x \in X \{y \in X \| \neg y R a\} = \{y \in X \| \neg y R x\})$
104	100 101 103	3syl	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to (\{y \in X \| \neg y R a\} \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) \leftrightarrow \exists x \in X \{y \in X \| \neg y R a\} = \{y \in X \| \neg y R x\})$
105	99 104	mpbird	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg y R a\} \in ran (x \in X ⟼ \{y \in X \| \neg y R x\})$
106	105 2	eleqtrrdi	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg y R a\} \in A$
107	5 106	sselid	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg y R a\} \in (A \cup B)$
108	95 107	sseldd	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg y R a\} \in fi (A \cup B)$
109		simprr	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to b \in X$
110		eqidd	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg b R y\} = \{y \in X \| \neg b R y\}$
111	64	rspceeqv	$⊢ (b \in X \land \{y \in X \| \neg b R y\} = \{y \in X \| \neg b R y\}) \to \exists x \in X \{y \in X \| \neg b R y\} = \{y \in X \| \neg x R y\}$
112	109 110 111	syl2anc	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \exists x \in X \{y \in X \| \neg b R y\} = \{y \in X \| \neg x R y\}$
113		rabexg	$⊢ X \in V \to \{y \in X \| \neg b R y\} \in V$
114		eqid	$⊢ (x \in X ⟼ \{y \in X \| \neg x R y\}) = (x \in X ⟼ \{y \in X \| \neg x R y\})$
115	114	elrnmpt	$⊢ \{y \in X \| \neg b R y\} \in V \to (\{y \in X \| \neg b R y\} \in ran (x \in X ⟼ \{y \in X \| \neg x R y\}) \leftrightarrow \exists x \in X \{y \in X \| \neg b R y\} = \{y \in X \| \neg x R y\})$
116	100 113 115	3syl	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to (\{y \in X \| \neg b R y\} \in ran (x \in X ⟼ \{y \in X \| \neg x R y\}) \leftrightarrow \exists x \in X \{y \in X \| \neg b R y\} = \{y \in X \| \neg x R y\})$
117	112 116	mpbird	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg b R y\} \in ran (x \in X ⟼ \{y \in X \| \neg x R y\})$
118	117 3	eleqtrrdi	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg b R y\} \in B$
119	17 118	sselid	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg b R y\} \in (A \cup B)$
120	95 119	sseldd	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg b R y\} \in fi (A \cup B)$
121		fiin	$⊢ (\{y \in X \| \neg y R a\} \in fi (A \cup B) \land \{y \in X \| \neg b R y\} \in fi (A \cup B)) \to \{y \in X \| \neg y R a\} \cap \{y \in X \| \neg b R y\} \in fi (A \cup B)$
122	108 120 121	syl2anc	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg y R a\} \cap \{y \in X \| \neg b R y\} \in fi (A \cup B)$
123	72 122	eqeltrrid	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| (\neg y R a \land \neg b R y)\} \in fi (A \cup B)$
124	123	ralrimivva	$⊢ R \in TosetRel \to \forall a \in X \forall b \in X \{y \in X \| (\neg y R a \land \neg b R y)\} \in fi (A \cup B)$
125	81	fmpo	$⊢ \forall a \in X \forall b \in X \{y \in X \| (\neg y R a \land \neg b R y)\} \in fi (A \cup B) \leftrightarrow (a \in X, b \in X ⟼ \{y \in X \| (\neg y R a \land \neg b R y)\}) : X \times X ⟶ fi (A \cup B)$
126	124 125	sylib	$⊢ R \in TosetRel \to (a \in X, b \in X ⟼ \{y \in X \| (\neg y R a \land \neg b R y)\}) : X \times X ⟶ fi (A \cup B)$
127	126	frnd	$⊢ R \in TosetRel \to ran (a \in X, b \in X ⟼ \{y \in X \| (\neg y R a \land \neg b R y)\}) \subseteq fi (A \cup B)$
128	4 127	eqsstrid	$⊢ R \in TosetRel \to C \subseteq fi (A \cup B)$
129	94 128	unssd	$⊢ R \in TosetRel \to (A \cup B) \cup C \subseteq fi (A \cup B)$
130	92 129	eqssd	$⊢ R \in TosetRel \to fi (A \cup B) = (A \cup B) \cup C$

Metamath Proof Explorer

Theorem ordtbas2

Proof