Metamath Proof Explorer

Theorem oeeulem

Description: Lemma for oeeu . (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Hypothesis oeeu.1 ⊢ X = ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
Assertion oeeulem ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → X ∈ On ∧ A ↑ 𝑜 X ⊆ B ∧ B ∈ A ↑ 𝑜 suc ⁡ X

Proof

Step Hyp Ref Expression
1 oeeu.1 ⊢ X = ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
2 eldifi ⊢ B ∈ On ∖ 1 𝑜 → B ∈ On
3 2 adantl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → B ∈ On
4 onsuc ⊢ B ∈ On → suc ⁡ B ∈ On
5 3 4 syl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → suc ⁡ B ∈ On
6 oeworde ⊢ A ∈ On ∖ 2 𝑜 ∧ suc ⁡ B ∈ On → suc ⁡ B ⊆ A ↑ 𝑜 suc ⁡ B
7 5 6 syldan ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → suc ⁡ B ⊆ A ↑ 𝑜 suc ⁡ B
8 sucidg ⊢ B ∈ On → B ∈ suc ⁡ B
9 3 8 syl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → B ∈ suc ⁡ B
10 7 9 sseldd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → B ∈ A ↑ 𝑜 suc ⁡ B
11 oveq2 ⊢ x = suc ⁡ B → A ↑ 𝑜 x = A ↑ 𝑜 suc ⁡ B
12 11 eleq2d ⊢ x = suc ⁡ B → B ∈ A ↑ 𝑜 x ↔ B ∈ A ↑ 𝑜 suc ⁡ B
13 12 rspcev ⊢ suc ⁡ B ∈ On ∧ B ∈ A ↑ 𝑜 suc ⁡ B → ∃ x ∈ On B ∈ A ↑ 𝑜 x
14 5 10 13 syl2anc ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ∃ x ∈ On B ∈ A ↑ 𝑜 x
15 onintrab2 ⊢ ∃ x ∈ On B ∈ A ↑ 𝑜 x ↔ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∈ On
16 14 15 sylib ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∈ On
17 onuni ⊢ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∈ On → ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∈ On
18 16 17 syl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∈ On
19 1 18 eqeltrid ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → X ∈ On
20 sucidg ⊢ X ∈ On → X ∈ suc ⁡ X
21 19 20 syl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → X ∈ suc ⁡ X
22 suceq ⊢ X = ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → suc ⁡ X = suc ⁡ ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
23 1 22 ax-mp ⊢ suc ⁡ X = suc ⁡ ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
24 dif1o ⊢ B ∈ On ∖ 1 𝑜 ↔ B ∈ On ∧ B ≠ ∅
25 24 simprbi ⊢ B ∈ On ∖ 1 𝑜 → B ≠ ∅
26 25 adantl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → B ≠ ∅
27 ssrab2 ⊢ x ∈ On | B ∈ A ↑ 𝑜 x ⊆ On
28 rabn0 ⊢ x ∈ On | B ∈ A ↑ 𝑜 x ≠ ∅ ↔ ∃ x ∈ On B ∈ A ↑ 𝑜 x
29 14 28 sylibr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → x ∈ On | B ∈ A ↑ 𝑜 x ≠ ∅
30 onint ⊢ x ∈ On | B ∈ A ↑ 𝑜 x ⊆ On ∧ x ∈ On | B ∈ A ↑ 𝑜 x ≠ ∅ → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∈ x ∈ On | B ∈ A ↑ 𝑜 x
31 27 29 30 sylancr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∈ x ∈ On | B ∈ A ↑ 𝑜 x
32 eleq1 ⊢ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ∅ → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∈ x ∈ On | B ∈ A ↑ 𝑜 x ↔ ∅ ∈ x ∈ On | B ∈ A ↑ 𝑜 x
33 31 32 syl5ibcom ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ∅ → ∅ ∈ x ∈ On | B ∈ A ↑ 𝑜 x
34 oveq2 ⊢ x = ∅ → A ↑ 𝑜 x = A ↑ 𝑜 ∅
35 34 eleq2d ⊢ x = ∅ → B ∈ A ↑ 𝑜 x ↔ B ∈ A ↑ 𝑜 ∅
36 35 elrab ⊢ ∅ ∈ x ∈ On | B ∈ A ↑ 𝑜 x ↔ ∅ ∈ On ∧ B ∈ A ↑ 𝑜 ∅
37 36 simprbi ⊢ ∅ ∈ x ∈ On | B ∈ A ↑ 𝑜 x → B ∈ A ↑ 𝑜 ∅
38 eldifi ⊢ A ∈ On ∖ 2 𝑜 → A ∈ On
39 38 adantr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → A ∈ On
40 oe0 ⊢ A ∈ On → A ↑ 𝑜 ∅ = 1 𝑜
41 39 40 syl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → A ↑ 𝑜 ∅ = 1 𝑜
42 41 eleq2d ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → B ∈ A ↑ 𝑜 ∅ ↔ B ∈ 1 𝑜
43 el1o ⊢ B ∈ 1 𝑜 ↔ B = ∅
44 42 43 bitrdi ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → B ∈ A ↑ 𝑜 ∅ ↔ B = ∅
45 37 44 imbitrid ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ∅ ∈ x ∈ On | B ∈ A ↑ 𝑜 x → B = ∅
46 33 45 syld ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ∅ → B = ∅
47 46 necon3ad ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → B ≠ ∅ → ¬ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ∅
48 26 47 mpd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ¬ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ∅
49 limuni ⊢ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
50 49 1 eqtr4di ⊢ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = X
51 50 adantl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = X
52 31 adantr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∈ x ∈ On | B ∈ A ↑ 𝑜 x
53 51 52 eqeltrrd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → X ∈ x ∈ On | B ∈ A ↑ 𝑜 x
54 oveq2 ⊢ y = X → A ↑ 𝑜 y = A ↑ 𝑜 X
55 54 eleq2d ⊢ y = X → B ∈ A ↑ 𝑜 y ↔ B ∈ A ↑ 𝑜 X
56 oveq2 ⊢ x = y → A ↑ 𝑜 x = A ↑ 𝑜 y
57 56 eleq2d ⊢ x = y → B ∈ A ↑ 𝑜 x ↔ B ∈ A ↑ 𝑜 y
58 57 cbvrabv ⊢ x ∈ On | B ∈ A ↑ 𝑜 x = y ∈ On | B ∈ A ↑ 𝑜 y
59 55 58 elrab2 ⊢ X ∈ x ∈ On | B ∈ A ↑ 𝑜 x ↔ X ∈ On ∧ B ∈ A ↑ 𝑜 X
60 59 simprbi ⊢ X ∈ x ∈ On | B ∈ A ↑ 𝑜 x → B ∈ A ↑ 𝑜 X
61 53 60 syl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → B ∈ A ↑ 𝑜 X
62 38 ad2antrr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → A ∈ On
63 limeq ⊢ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = X → Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ↔ Lim ⁡ X
64 50 63 syl ⊢ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ↔ Lim ⁡ X
65 64 ibi ⊢ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → Lim ⁡ X
66 19 65 anim12i ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → X ∈ On ∧ Lim ⁡ X
67 dif20el ⊢ A ∈ On ∖ 2 𝑜 → ∅ ∈ A
68 67 ad2antrr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → ∅ ∈ A
69 oelim ⊢ A ∈ On ∧ X ∈ On ∧ Lim ⁡ X ∧ ∅ ∈ A → A ↑ 𝑜 X = ⋃ y ∈ X A ↑ 𝑜 y
70 62 66 68 69 syl21anc ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → A ↑ 𝑜 X = ⋃ y ∈ X A ↑ 𝑜 y
71 61 70 eleqtrd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → B ∈ ⋃ y ∈ X A ↑ 𝑜 y
72 eliun ⊢ B ∈ ⋃ y ∈ X A ↑ 𝑜 y ↔ ∃ y ∈ X B ∈ A ↑ 𝑜 y
73 71 72 sylib ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → ∃ y ∈ X B ∈ A ↑ 𝑜 y
74 19 adantr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → X ∈ On
75 onss ⊢ X ∈ On → X ⊆ On
76 74 75 syl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → X ⊆ On
77 76 sselda ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∧ y ∈ X → y ∈ On
78 51 eleq2d ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → y ∈ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ↔ y ∈ X
79 78 biimpar ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∧ y ∈ X → y ∈ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
80 57 onnminsb ⊢ y ∈ On → y ∈ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → ¬ B ∈ A ↑ 𝑜 y
81 77 79 80 sylc ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∧ y ∈ X → ¬ B ∈ A ↑ 𝑜 y
82 81 nrexdv ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 ∧ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → ¬ ∃ y ∈ X B ∈ A ↑ 𝑜 y
83 73 82 pm2.65da ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ¬ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
84 ioran ⊢ ¬ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ∅ ∨ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ↔ ¬ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ∅ ∧ ¬ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
85 48 83 84 sylanbrc ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ¬ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ∅ ∨ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
86 eloni ⊢ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∈ On → Ord ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
87 unizlim ⊢ Ord ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ↔ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ∅ ∨ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
88 16 86 87 3syl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ↔ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ∅ ∨ Lim ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
89 85 88 mtbird ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ¬ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
90 orduniorsuc ⊢ Ord ⁡ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∨ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = suc ⁡ ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
91 16 86 90 3syl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x ∨ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = suc ⁡ ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
92 91 ord ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ¬ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = suc ⁡ ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
93 89 92 mpd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = suc ⁡ ⋃ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
94 23 93 eqtr4id ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → suc ⁡ X = ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
95 21 94 eleqtrd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → X ∈ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x
96 58 inteqi ⊢ ⋂ x ∈ On | B ∈ A ↑ 𝑜 x = ⋂ y ∈ On | B ∈ A ↑ 𝑜 y
97 95 96 eleqtrdi ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → X ∈ ⋂ y ∈ On | B ∈ A ↑ 𝑜 y
98 55 onnminsb ⊢ X ∈ On → X ∈ ⋂ y ∈ On | B ∈ A ↑ 𝑜 y → ¬ B ∈ A ↑ 𝑜 X
99 19 97 98 sylc ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → ¬ B ∈ A ↑ 𝑜 X
100 oecl ⊢ A ∈ On ∧ X ∈ On → A ↑ 𝑜 X ∈ On
101 39 19 100 syl2anc ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → A ↑ 𝑜 X ∈ On
102 ontri1 ⊢ A ↑ 𝑜 X ∈ On ∧ B ∈ On → A ↑ 𝑜 X ⊆ B ↔ ¬ B ∈ A ↑ 𝑜 X
103 101 3 102 syl2anc ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → A ↑ 𝑜 X ⊆ B ↔ ¬ B ∈ A ↑ 𝑜 X
104 99 103 mpbird ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → A ↑ 𝑜 X ⊆ B
105 94 31 eqeltrd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → suc ⁡ X ∈ x ∈ On | B ∈ A ↑ 𝑜 x
106 oveq2 ⊢ y = suc ⁡ X → A ↑ 𝑜 y = A ↑ 𝑜 suc ⁡ X
107 106 eleq2d ⊢ y = suc ⁡ X → B ∈ A ↑ 𝑜 y ↔ B ∈ A ↑ 𝑜 suc ⁡ X
108 107 58 elrab2 ⊢ suc ⁡ X ∈ x ∈ On | B ∈ A ↑ 𝑜 x ↔ suc ⁡ X ∈ On ∧ B ∈ A ↑ 𝑜 suc ⁡ X
109 108 simprbi ⊢ suc ⁡ X ∈ x ∈ On | B ∈ A ↑ 𝑜 x → B ∈ A ↑ 𝑜 suc ⁡ X
110 105 109 syl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → B ∈ A ↑ 𝑜 suc ⁡ X
111 19 104 110 3jca ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∖ 1 𝑜 → X ∈ On ∧ A ↑ 𝑜 X ⊆ B ∧ B ∈ A ↑ 𝑜 suc ⁡ X