Metamath Proof Explorer

Theorem oawordeulem

Description: Lemma for oawordex . (Contributed by NM, 11-Dec-2004)

Ref Expression
Hypotheses oawordeulem.1 ⊢ 𝐴 ∈ On
oawordeulem.2 ⊢ 𝐵 ∈ On
oawordeulem.3 ⊢ 𝑆 = { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) }
Assertion oawordeulem ( 𝐴 ⊆ 𝐵 → ∃! 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 oawordeulem.1 ⊢ 𝐴 ∈ On
2 oawordeulem.2 ⊢ 𝐵 ∈ On
3 oawordeulem.3 ⊢ 𝑆 = { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) }
4 3 ssrab3 ⊢ 𝑆 ⊆ On
5 oaword2 ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → 𝐵 ⊆ ( 𝐴 +o 𝐵 ) )
6 2 1 5 mp2an ⊢ 𝐵 ⊆ ( 𝐴 +o 𝐵 )
7 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 +o 𝑦 ) = ( 𝐴 +o 𝐵 ) )
8 7 sseq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐵 ⊆ ( 𝐴 +o 𝑦 ) ↔ 𝐵 ⊆ ( 𝐴 +o 𝐵 ) ) )
9 8 3 elrab2 ⊢ ( 𝐵 ∈ 𝑆 ↔ ( 𝐵 ∈ On ∧ 𝐵 ⊆ ( 𝐴 +o 𝐵 ) ) )
10 2 6 9 mpbir2an ⊢ 𝐵 ∈ 𝑆
11 10 ne0ii ⊢ 𝑆 ≠ ∅
12 oninton ⊢ ( ( 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ On )
13 4 11 12 mp2an ⊢ ∩ 𝑆 ∈ On
14 onzsl ⊢ ( ∩ 𝑆 ∈ On ↔ ( ∩ 𝑆 = ∅ ∨ ∃ 𝑧 ∈ On ∩ 𝑆 = suc 𝑧 ∨ ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) ) )
15 13 14 mpbi ⊢ ( ∩ 𝑆 = ∅ ∨ ∃ 𝑧 ∈ On ∩ 𝑆 = suc 𝑧 ∨ ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) )
16 oveq2 ⊢ ( ∩ 𝑆 = ∅ → ( 𝐴 +o ∩ 𝑆 ) = ( 𝐴 +o ∅ ) )
17 oa0 ⊢ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = 𝐴 )
18 1 17 ax-mp ⊢ ( 𝐴 +o ∅ ) = 𝐴
19 16 18 eqtrdi ⊢ ( ∩ 𝑆 = ∅ → ( 𝐴 +o ∩ 𝑆 ) = 𝐴 )
20 19 sseq1d ⊢ ( ∩ 𝑆 = ∅ → ( ( 𝐴 +o ∩ 𝑆 ) ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )
21 20 biimprd ⊢ ( ∩ 𝑆 = ∅ → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +o ∩ 𝑆 ) ⊆ 𝐵 ) )
22 oveq2 ⊢ ( ∩ 𝑆 = suc 𝑧 → ( 𝐴 +o ∩ 𝑆 ) = ( 𝐴 +o suc 𝑧 ) )
23 oasuc ⊢ ( ( 𝐴 ∈ On ∧ 𝑧 ∈ On ) → ( 𝐴 +o suc 𝑧 ) = suc ( 𝐴 +o 𝑧 ) )
24 1 23 mpan ⊢ ( 𝑧 ∈ On → ( 𝐴 +o suc 𝑧 ) = suc ( 𝐴 +o 𝑧 ) )
25 22 24 sylan9eqr ⊢ ( ( 𝑧 ∈ On ∧ ∩ 𝑆 = suc 𝑧 ) → ( 𝐴 +o ∩ 𝑆 ) = suc ( 𝐴 +o 𝑧 ) )
26 vex ⊢ 𝑧 ∈ V
27 26 sucid ⊢ 𝑧 ∈ suc 𝑧
28 eleq2 ⊢ ( ∩ 𝑆 = suc 𝑧 → ( 𝑧 ∈ ∩ 𝑆 ↔ 𝑧 ∈ suc 𝑧 ) )
29 27 28 mpbiri ⊢ ( ∩ 𝑆 = suc 𝑧 → 𝑧 ∈ ∩ 𝑆 )
30 13 oneli ⊢ ( 𝑧 ∈ ∩ 𝑆 → 𝑧 ∈ On )
31 3 inteqi ⊢ ∩ 𝑆 = ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) }
32 31 eleq2i ⊢ ( 𝑧 ∈ ∩ 𝑆 ↔ 𝑧 ∈ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } )
33 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐴 +o 𝑦 ) = ( 𝐴 +o 𝑧 ) )
34 33 sseq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐵 ⊆ ( 𝐴 +o 𝑦 ) ↔ 𝐵 ⊆ ( 𝐴 +o 𝑧 ) ) )
35 34 onnminsb ⊢ ( 𝑧 ∈ On → ( 𝑧 ∈ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } → ¬ 𝐵 ⊆ ( 𝐴 +o 𝑧 ) ) )
36 32 35 biimtrid ⊢ ( 𝑧 ∈ On → ( 𝑧 ∈ ∩ 𝑆 → ¬ 𝐵 ⊆ ( 𝐴 +o 𝑧 ) ) )
37 oacl ⊢ ( ( 𝐴 ∈ On ∧ 𝑧 ∈ On ) → ( 𝐴 +o 𝑧 ) ∈ On )
38 1 37 mpan ⊢ ( 𝑧 ∈ On → ( 𝐴 +o 𝑧 ) ∈ On )
39 ontri1 ⊢ ( ( 𝐵 ∈ On ∧ ( 𝐴 +o 𝑧 ) ∈ On ) → ( 𝐵 ⊆ ( 𝐴 +o 𝑧 ) ↔ ¬ ( 𝐴 +o 𝑧 ) ∈ 𝐵 ) )
40 2 38 39 sylancr ⊢ ( 𝑧 ∈ On → ( 𝐵 ⊆ ( 𝐴 +o 𝑧 ) ↔ ¬ ( 𝐴 +o 𝑧 ) ∈ 𝐵 ) )
41 40 con2bid ⊢ ( 𝑧 ∈ On → ( ( 𝐴 +o 𝑧 ) ∈ 𝐵 ↔ ¬ 𝐵 ⊆ ( 𝐴 +o 𝑧 ) ) )
42 36 41 sylibrd ⊢ ( 𝑧 ∈ On → ( 𝑧 ∈ ∩ 𝑆 → ( 𝐴 +o 𝑧 ) ∈ 𝐵 ) )
43 30 42 mpcom ⊢ ( 𝑧 ∈ ∩ 𝑆 → ( 𝐴 +o 𝑧 ) ∈ 𝐵 )
44 2 onordi ⊢ Ord 𝐵
45 ordsucss ⊢ ( Ord 𝐵 → ( ( 𝐴 +o 𝑧 ) ∈ 𝐵 → suc ( 𝐴 +o 𝑧 ) ⊆ 𝐵 ) )
46 44 45 ax-mp ⊢ ( ( 𝐴 +o 𝑧 ) ∈ 𝐵 → suc ( 𝐴 +o 𝑧 ) ⊆ 𝐵 )
47 29 43 46 3syl ⊢ ( ∩ 𝑆 = suc 𝑧 → suc ( 𝐴 +o 𝑧 ) ⊆ 𝐵 )
48 47 adantl ⊢ ( ( 𝑧 ∈ On ∧ ∩ 𝑆 = suc 𝑧 ) → suc ( 𝐴 +o 𝑧 ) ⊆ 𝐵 )
49 25 48 eqsstrd ⊢ ( ( 𝑧 ∈ On ∧ ∩ 𝑆 = suc 𝑧 ) → ( 𝐴 +o ∩ 𝑆 ) ⊆ 𝐵 )
50 49 rexlimiva ⊢ ( ∃ 𝑧 ∈ On ∩ 𝑆 = suc 𝑧 → ( 𝐴 +o ∩ 𝑆 ) ⊆ 𝐵 )
51 50 a1d ⊢ ( ∃ 𝑧 ∈ On ∩ 𝑆 = suc 𝑧 → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +o ∩ 𝑆 ) ⊆ 𝐵 ) )
52 oalim ⊢ ( ( 𝐴 ∈ On ∧ ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) ) → ( 𝐴 +o ∩ 𝑆 ) = ∪ 𝑧 ∈ ∩ 𝑆 ( 𝐴 +o 𝑧 ) )
53 1 52 mpan ⊢ ( ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) → ( 𝐴 +o ∩ 𝑆 ) = ∪ 𝑧 ∈ ∩ 𝑆 ( 𝐴 +o 𝑧 ) )
54 iunss ⊢ ( ∪ 𝑧 ∈ ∩ 𝑆 ( 𝐴 +o 𝑧 ) ⊆ 𝐵 ↔ ∀ 𝑧 ∈ ∩ 𝑆 ( 𝐴 +o 𝑧 ) ⊆ 𝐵 )
55 2 onelssi ⊢ ( ( 𝐴 +o 𝑧 ) ∈ 𝐵 → ( 𝐴 +o 𝑧 ) ⊆ 𝐵 )
56 43 55 syl ⊢ ( 𝑧 ∈ ∩ 𝑆 → ( 𝐴 +o 𝑧 ) ⊆ 𝐵 )
57 54 56 mprgbir ⊢ ∪ 𝑧 ∈ ∩ 𝑆 ( 𝐴 +o 𝑧 ) ⊆ 𝐵
58 53 57 eqsstrdi ⊢ ( ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) → ( 𝐴 +o ∩ 𝑆 ) ⊆ 𝐵 )
59 58 a1d ⊢ ( ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +o ∩ 𝑆 ) ⊆ 𝐵 ) )
60 21 51 59 3jaoi ⊢ ( ( ∩ 𝑆 = ∅ ∨ ∃ 𝑧 ∈ On ∩ 𝑆 = suc 𝑧 ∨ ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +o ∩ 𝑆 ) ⊆ 𝐵 ) )
61 15 60 ax-mp ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 +o ∩ 𝑆 ) ⊆ 𝐵 )
62 8 rspcev ⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ⊆ ( 𝐴 +o 𝐵 ) ) → ∃ 𝑦 ∈ On 𝐵 ⊆ ( 𝐴 +o 𝑦 ) )
63 2 6 62 mp2an ⊢ ∃ 𝑦 ∈ On 𝐵 ⊆ ( 𝐴 +o 𝑦 )
64 nfcv ⊢ Ⅎ 𝑦 𝐵
65 nfcv ⊢ Ⅎ 𝑦 𝐴
66 nfcv ⊢ Ⅎ 𝑦 +o
67 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) }
68 67 nfint ⊢ Ⅎ 𝑦 ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) }
69 65 66 68 nfov ⊢ Ⅎ 𝑦 ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } )
70 64 69 nfss ⊢ Ⅎ 𝑦 𝐵 ⊆ ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } )
71 oveq2 ⊢ ( 𝑦 = ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } → ( 𝐴 +o 𝑦 ) = ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) )
72 71 sseq2d ⊢ ( 𝑦 = ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } → ( 𝐵 ⊆ ( 𝐴 +o 𝑦 ) ↔ 𝐵 ⊆ ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) ) )
73 70 72 onminsb ⊢ ( ∃ 𝑦 ∈ On 𝐵 ⊆ ( 𝐴 +o 𝑦 ) → 𝐵 ⊆ ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) )
74 63 73 ax-mp ⊢ 𝐵 ⊆ ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } )
75 31 oveq2i ⊢ ( 𝐴 +o ∩ 𝑆 ) = ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } )
76 74 75 sseqtrri ⊢ 𝐵 ⊆ ( 𝐴 +o ∩ 𝑆 )
77 eqss ⊢ ( ( 𝐴 +o ∩ 𝑆 ) = 𝐵 ↔ ( ( 𝐴 +o ∩ 𝑆 ) ⊆ 𝐵 ∧ 𝐵 ⊆ ( 𝐴 +o ∩ 𝑆 ) ) )
78 61 76 77 sylanblrc ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 +o ∩ 𝑆 ) = 𝐵 )
79 oveq2 ⊢ ( 𝑥 = ∩ 𝑆 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o ∩ 𝑆 ) )
80 79 eqeq1d ⊢ ( 𝑥 = ∩ 𝑆 → ( ( 𝐴 +o 𝑥 ) = 𝐵 ↔ ( 𝐴 +o ∩ 𝑆 ) = 𝐵 ) )
81 80 rspcev ⊢ ( ( ∩ 𝑆 ∈ On ∧ ( 𝐴 +o ∩ 𝑆 ) = 𝐵 ) → ∃ 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 )
82 13 78 81 sylancr ⊢ ( 𝐴 ⊆ 𝐵 → ∃ 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 )
83 eqtr3 ⊢ ( ( ( 𝐴 +o 𝑥 ) = 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) )
84 oacan ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) ↔ 𝑥 = 𝑦 ) )
85 1 84 mp3an1 ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) ↔ 𝑥 = 𝑦 ) )
86 83 85 imbitrid ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( ( 𝐴 +o 𝑥 ) = 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) → 𝑥 = 𝑦 ) )
87 86 rgen2 ⊢ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( ( ( 𝐴 +o 𝑥 ) = 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) → 𝑥 = 𝑦 )
88 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) )
89 88 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 +o 𝑥 ) = 𝐵 ↔ ( 𝐴 +o 𝑦 ) = 𝐵 ) )
90 89 reu4 ⊢ ( ∃! 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 ↔ ( ∃ 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 ∧ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( ( ( 𝐴 +o 𝑥 ) = 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐵 ) → 𝑥 = 𝑦 ) ) )
91 82 87 90 sylanblrc ⊢ ( 𝐴 ⊆ 𝐵 → ∃! 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 )