Metamath Proof Explorer

Theorem nnawordex

Description: Equivalence for weak ordering of natural numbers. (Contributed by NM, 8-Nov-2002) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnawordex ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 +o 𝑦 ) = ( 𝐴 +o 𝐵 ) )
2 1 sseq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐵 ⊆ ( 𝐴 +o 𝑦 ) ↔ 𝐵 ⊆ ( 𝐴 +o 𝐵 ) ) )
3 simplr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 ∈ ω )
4 nnon ⊢ ( 𝐵 ∈ ω → 𝐵 ∈ On )
5 3 4 syl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 ∈ On )
6 simpll ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ∈ ω )
7 nnaword2 ⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) → 𝐵 ⊆ ( 𝐴 +o 𝐵 ) )
8 3 6 7 syl2anc ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 ⊆ ( 𝐴 +o 𝐵 ) )
9 2 5 8 elrabd ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 ∈ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } )
10 intss1 ⊢ ( 𝐵 ∈ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } → ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ⊆ 𝐵 )
11 9 10 syl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ⊆ 𝐵 )
12 ssrab2 ⊢ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ⊆ On
13 9 ne0d ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ≠ ∅ )
14 oninton ⊢ ( ( { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ⊆ On ∧ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ≠ ∅ ) → ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∈ On )
15 12 13 14 sylancr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∈ On )
16 eloni ⊢ ( ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∈ On → Ord ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } )
17 15 16 syl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → Ord ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } )
18 ordom ⊢ Ord ω
19 ordtr2 ⊢ ( ( Ord ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∧ Ord ω ) → ( ( ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ⊆ 𝐵 ∧ 𝐵 ∈ ω ) → ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∈ ω ) )
20 17 18 19 sylancl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ⊆ 𝐵 ∧ 𝐵 ∈ ω ) → ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∈ ω ) )
21 11 3 20 mp2and ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∈ ω )
22 nna0 ⊢ ( 𝐴 ∈ ω → ( 𝐴 +o ∅ ) = 𝐴 )
23 22 ad2antrr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 +o ∅ ) = 𝐴 )
24 simpr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ 𝐵 )
25 23 24 eqsstrd ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 +o ∅ ) ⊆ 𝐵 )
26 oveq2 ⊢ ( ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = ∅ → ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) = ( 𝐴 +o ∅ ) )
27 26 sseq1d ⊢ ( ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = ∅ → ( ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) ⊆ 𝐵 ↔ ( 𝐴 +o ∅ ) ⊆ 𝐵 ) )
28 25 27 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → ( ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = ∅ → ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) ⊆ 𝐵 ) )
29 simprr ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 )
30 29 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) = ( 𝐴 +o suc 𝑥 ) )
31 6 adantr ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → 𝐴 ∈ ω )
32 simprl ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → 𝑥 ∈ ω )
33 nnasuc ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ( 𝐴 +o suc 𝑥 ) = suc ( 𝐴 +o 𝑥 ) )
34 31 32 33 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → ( 𝐴 +o suc 𝑥 ) = suc ( 𝐴 +o 𝑥 ) )
35 30 34 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) = suc ( 𝐴 +o 𝑥 ) )
36 nnord ⊢ ( 𝐵 ∈ ω → Ord 𝐵 )
37 3 36 syl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → Ord 𝐵 )
38 37 adantr ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → Ord 𝐵 )
39 nnon ⊢ ( 𝑥 ∈ ω → 𝑥 ∈ On )
40 39 adantr ⊢ ( ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) → 𝑥 ∈ On )
41 vex ⊢ 𝑥 ∈ V
42 41 sucid ⊢ 𝑥 ∈ suc 𝑥
43 simpr ⊢ ( ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) → ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 )
44 42 43 eleqtrrid ⊢ ( ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) → 𝑥 ∈ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } )
45 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐴 +o 𝑦 ) = ( 𝐴 +o 𝑥 ) )
46 45 sseq2d ⊢ ( 𝑦 = 𝑥 → ( 𝐵 ⊆ ( 𝐴 +o 𝑦 ) ↔ 𝐵 ⊆ ( 𝐴 +o 𝑥 ) ) )
47 46 onnminsb ⊢ ( 𝑥 ∈ On → ( 𝑥 ∈ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } → ¬ 𝐵 ⊆ ( 𝐴 +o 𝑥 ) ) )
48 40 44 47 sylc ⊢ ( ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) → ¬ 𝐵 ⊆ ( 𝐴 +o 𝑥 ) )
49 48 adantl ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → ¬ 𝐵 ⊆ ( 𝐴 +o 𝑥 ) )
50 nnacl ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ( 𝐴 +o 𝑥 ) ∈ ω )
51 31 32 50 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → ( 𝐴 +o 𝑥 ) ∈ ω )
52 nnord ⊢ ( ( 𝐴 +o 𝑥 ) ∈ ω → Ord ( 𝐴 +o 𝑥 ) )
53 51 52 syl ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → Ord ( 𝐴 +o 𝑥 ) )
54 ordtri1 ⊢ ( ( Ord 𝐵 ∧ Ord ( 𝐴 +o 𝑥 ) ) → ( 𝐵 ⊆ ( 𝐴 +o 𝑥 ) ↔ ¬ ( 𝐴 +o 𝑥 ) ∈ 𝐵 ) )
55 38 53 54 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → ( 𝐵 ⊆ ( 𝐴 +o 𝑥 ) ↔ ¬ ( 𝐴 +o 𝑥 ) ∈ 𝐵 ) )
56 55 con2bid ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → ( ( 𝐴 +o 𝑥 ) ∈ 𝐵 ↔ ¬ 𝐵 ⊆ ( 𝐴 +o 𝑥 ) ) )
57 49 56 mpbird ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → ( 𝐴 +o 𝑥 ) ∈ 𝐵 )
58 ordsucss ⊢ ( Ord 𝐵 → ( ( 𝐴 +o 𝑥 ) ∈ 𝐵 → suc ( 𝐴 +o 𝑥 ) ⊆ 𝐵 ) )
59 38 57 58 sylc ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → suc ( 𝐴 +o 𝑥 ) ⊆ 𝐵 )
60 35 59 eqsstrd ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ω ∧ ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) ) → ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) ⊆ 𝐵 )
61 60 rexlimdvaa ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → ( ∃ 𝑥 ∈ ω ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 → ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) ⊆ 𝐵 ) )
62 nn0suc ⊢ ( ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∈ ω → ( ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = ∅ ∨ ∃ 𝑥 ∈ ω ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) )
63 21 62 syl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → ( ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = ∅ ∨ ∃ 𝑥 ∈ ω ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } = suc 𝑥 ) )
64 28 61 63 mpjaod ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) ⊆ 𝐵 )
65 onint ⊢ ( ( { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ⊆ On ∧ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ≠ ∅ ) → ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∈ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } )
66 12 13 65 sylancr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∈ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } )
67 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) }
68 67 nfint ⊢ Ⅎ 𝑦 ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) }
69 nfcv ⊢ Ⅎ 𝑦 On
70 nfcv ⊢ Ⅎ 𝑦 𝐵
71 nfcv ⊢ Ⅎ 𝑦 𝐴
72 nfcv ⊢ Ⅎ 𝑦 +o
73 71 72 68 nfov ⊢ Ⅎ 𝑦 ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } )
74 70 73 nfss ⊢ Ⅎ 𝑦 𝐵 ⊆ ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } )
75 oveq2 ⊢ ( 𝑦 = ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } → ( 𝐴 +o 𝑦 ) = ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) )
76 75 sseq2d ⊢ ( 𝑦 = ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } → ( 𝐵 ⊆ ( 𝐴 +o 𝑦 ) ↔ 𝐵 ⊆ ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) ) )
77 68 69 74 76 elrabf ⊢ ( ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∈ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ↔ ( ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∈ On ∧ 𝐵 ⊆ ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) ) )
78 77 simprbi ⊢ ( ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∈ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } → 𝐵 ⊆ ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) )
79 66 78 syl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 ⊆ ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) )
80 64 79 eqssd ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) = 𝐵 )
81 oveq2 ⊢ ( 𝑥 = ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) )
82 81 eqeq1d ⊢ ( 𝑥 = ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } → ( ( 𝐴 +o 𝑥 ) = 𝐵 ↔ ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) = 𝐵 ) )
83 82 rspcev ⊢ ( ( ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ∈ ω ∧ ( 𝐴 +o ∩ { 𝑦 ∈ On ∣ 𝐵 ⊆ ( 𝐴 +o 𝑦 ) } ) = 𝐵 ) → ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 )
84 21 80 83 syl2anc ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐴 ⊆ 𝐵 ) → ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 )
85 84 ex ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ⊆ 𝐵 → ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 ) )
86 nnaword1 ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → 𝐴 ⊆ ( 𝐴 +o 𝑥 ) )
87 86 adantlr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝑥 ∈ ω ) → 𝐴 ⊆ ( 𝐴 +o 𝑥 ) )
88 sseq2 ⊢ ( ( 𝐴 +o 𝑥 ) = 𝐵 → ( 𝐴 ⊆ ( 𝐴 +o 𝑥 ) ↔ 𝐴 ⊆ 𝐵 ) )
89 87 88 syl5ibcom ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝑥 ∈ ω ) → ( ( 𝐴 +o 𝑥 ) = 𝐵 → 𝐴 ⊆ 𝐵 ) )
90 89 rexlimdva ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 → 𝐴 ⊆ 𝐵 ) )
91 85 90 impbid ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) = 𝐵 ) )