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 syl5bi ( 𝑧 ∈ 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 syl5ib ( ( 𝑥 ∈ 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 𝑥 ) = 𝐵 )