Metamath Proof Explorer


Theorem ordtbas2

Description: Lemma for ordtbas . (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses ordtval.1 X = dom R
ordtval.2 A = ran x X y X | ¬ y R x
ordtval.3 B = ran x X y X | ¬ x R y
ordtval.4 C = ran a X , b X y X | ¬ y R a ¬ b R y
Assertion ordtbas2 R TosetRel fi A B = A B C

Proof

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