MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnawordex Structured version   Visualization version   GIF version

Theorem nnawordex 7964
Description: Equivalence for weak ordering of natural numbers. (Contributed by NM, 8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
Assertion
Ref Expression
nnawordex ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴𝐵 ↔ ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem nnawordex
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 simplr 776 . . . . . . . 8 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → 𝐵 ∈ ω)
2 nnon 7311 . . . . . . . 8 (𝐵 ∈ ω → 𝐵 ∈ On)
31, 2syl 17 . . . . . . 7 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → 𝐵 ∈ On)
4 simpll 774 . . . . . . . 8 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → 𝐴 ∈ ω)
5 nnaword2 7957 . . . . . . . 8 ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → 𝐵 ⊆ (𝐴 +𝑜 𝐵))
61, 4, 5syl2anc 575 . . . . . . 7 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → 𝐵 ⊆ (𝐴 +𝑜 𝐵))
7 oveq2 6892 . . . . . . . . 9 (𝑦 = 𝐵 → (𝐴 +𝑜 𝑦) = (𝐴 +𝑜 𝐵))
87sseq2d 3841 . . . . . . . 8 (𝑦 = 𝐵 → (𝐵 ⊆ (𝐴 +𝑜 𝑦) ↔ 𝐵 ⊆ (𝐴 +𝑜 𝐵)))
98elrab 3570 . . . . . . 7 (𝐵 ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ↔ (𝐵 ∈ On ∧ 𝐵 ⊆ (𝐴 +𝑜 𝐵)))
103, 6, 9sylanbrc 574 . . . . . 6 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → 𝐵 ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)})
11 intss1 4695 . . . . . 6 (𝐵 ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ 𝐵)
1210, 11syl 17 . . . . 5 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ 𝐵)
13 ssrab2 3895 . . . . . . . 8 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ On
1410ne0d 4134 . . . . . . . 8 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ≠ ∅)
15 oninton 7240 . . . . . . . 8 (({𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ≠ ∅) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ On)
1613, 14, 15sylancr 577 . . . . . . 7 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ On)
17 eloni 5960 . . . . . . 7 ( {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ On → Ord {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)})
1816, 17syl 17 . . . . . 6 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → Ord {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)})
19 ordom 7314 . . . . . 6 Ord ω
20 ordtr2 5994 . . . . . 6 ((Ord {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∧ Ord ω) → (( {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ 𝐵𝐵 ∈ ω) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ ω))
2118, 19, 20sylancl 576 . . . . 5 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → (( {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ 𝐵𝐵 ∈ ω) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ ω))
2212, 1, 21mp2and 682 . . . 4 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ ω)
23 nna0 7931 . . . . . . . . 9 (𝐴 ∈ ω → (𝐴 +𝑜 ∅) = 𝐴)
2423ad2antrr 708 . . . . . . . 8 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → (𝐴 +𝑜 ∅) = 𝐴)
25 simpr 473 . . . . . . . 8 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → 𝐴𝐵)
2624, 25eqsstrd 3847 . . . . . . 7 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → (𝐴 +𝑜 ∅) ⊆ 𝐵)
27 oveq2 6892 . . . . . . . 8 ( {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = ∅ → (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) = (𝐴 +𝑜 ∅))
2827sseq1d 3840 . . . . . . 7 ( {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = ∅ → ((𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) ⊆ 𝐵 ↔ (𝐴 +𝑜 ∅) ⊆ 𝐵))
2926, 28syl5ibrcom 238 . . . . . 6 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → ( {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = ∅ → (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) ⊆ 𝐵))
30 simprr 780 . . . . . . . . . 10 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)
3130oveq2d 6900 . . . . . . . . 9 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) = (𝐴 +𝑜 suc 𝑥))
324adantr 468 . . . . . . . . . 10 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → 𝐴 ∈ ω)
33 simprl 778 . . . . . . . . . 10 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → 𝑥 ∈ ω)
34 nnasuc 7933 . . . . . . . . . 10 ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +𝑜 suc 𝑥) = suc (𝐴 +𝑜 𝑥))
3532, 33, 34syl2anc 575 . . . . . . . . 9 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → (𝐴 +𝑜 suc 𝑥) = suc (𝐴 +𝑜 𝑥))
3631, 35eqtrd 2851 . . . . . . . 8 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) = suc (𝐴 +𝑜 𝑥))
37 nnord 7313 . . . . . . . . . . 11 (𝐵 ∈ ω → Ord 𝐵)
381, 37syl 17 . . . . . . . . . 10 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → Ord 𝐵)
3938adantr 468 . . . . . . . . 9 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → Ord 𝐵)
40 nnon 7311 . . . . . . . . . . . . 13 (𝑥 ∈ ω → 𝑥 ∈ On)
4140adantr 468 . . . . . . . . . . . 12 ((𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥) → 𝑥 ∈ On)
42 vex 3405 . . . . . . . . . . . . . 14 𝑥 ∈ V
4342sucid 6030 . . . . . . . . . . . . 13 𝑥 ∈ suc 𝑥
44 simpr 473 . . . . . . . . . . . . 13 ((𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)
4543, 44syl5eleqr 2903 . . . . . . . . . . . 12 ((𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥) → 𝑥 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)})
46 oveq2 6892 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝐴 +𝑜 𝑦) = (𝐴 +𝑜 𝑥))
4746sseq2d 3841 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (𝐵 ⊆ (𝐴 +𝑜 𝑦) ↔ 𝐵 ⊆ (𝐴 +𝑜 𝑥)))
4847onnminsb 7244 . . . . . . . . . . . 12 (𝑥 ∈ On → (𝑥 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → ¬ 𝐵 ⊆ (𝐴 +𝑜 𝑥)))
4941, 45, 48sylc 65 . . . . . . . . . . 11 ((𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥) → ¬ 𝐵 ⊆ (𝐴 +𝑜 𝑥))
5049adantl 469 . . . . . . . . . 10 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → ¬ 𝐵 ⊆ (𝐴 +𝑜 𝑥))
51 nnacl 7938 . . . . . . . . . . . . . 14 ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +𝑜 𝑥) ∈ ω)
5232, 33, 51syl2anc 575 . . . . . . . . . . . . 13 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → (𝐴 +𝑜 𝑥) ∈ ω)
53 nnord 7313 . . . . . . . . . . . . 13 ((𝐴 +𝑜 𝑥) ∈ ω → Ord (𝐴 +𝑜 𝑥))
5452, 53syl 17 . . . . . . . . . . . 12 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → Ord (𝐴 +𝑜 𝑥))
55 ordtri1 5983 . . . . . . . . . . . 12 ((Ord 𝐵 ∧ Ord (𝐴 +𝑜 𝑥)) → (𝐵 ⊆ (𝐴 +𝑜 𝑥) ↔ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐵))
5639, 54, 55syl2anc 575 . . . . . . . . . . 11 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → (𝐵 ⊆ (𝐴 +𝑜 𝑥) ↔ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐵))
5756con2bid 345 . . . . . . . . . 10 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → ((𝐴 +𝑜 𝑥) ∈ 𝐵 ↔ ¬ 𝐵 ⊆ (𝐴 +𝑜 𝑥)))
5850, 57mpbird 248 . . . . . . . . 9 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → (𝐴 +𝑜 𝑥) ∈ 𝐵)
59 ordsucss 7258 . . . . . . . . 9 (Ord 𝐵 → ((𝐴 +𝑜 𝑥) ∈ 𝐵 → suc (𝐴 +𝑜 𝑥) ⊆ 𝐵))
6039, 58, 59sylc 65 . . . . . . . 8 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → suc (𝐴 +𝑜 𝑥) ⊆ 𝐵)
6136, 60eqsstrd 3847 . . . . . . 7 ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) ∧ (𝑥 ∈ ω ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥)) → (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) ⊆ 𝐵)
6261rexlimdvaa 3231 . . . . . 6 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → (∃𝑥 ∈ ω {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥 → (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) ⊆ 𝐵))
63 nn0suc 7330 . . . . . . 7 ( {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ ω → ( {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = ∅ ∨ ∃𝑥 ∈ ω {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥))
6422, 63syl 17 . . . . . 6 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → ( {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = ∅ ∨ ∃𝑥 ∈ ω {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} = suc 𝑥))
6529, 62, 64mpjaod 878 . . . . 5 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) ⊆ 𝐵)
66 onint 7235 . . . . . . 7 (({𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ≠ ∅) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)})
6713, 14, 66sylancr 577 . . . . . 6 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)})
68 nfrab1 3322 . . . . . . . . 9 𝑦{𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}
6968nfint 4690 . . . . . . . 8 𝑦 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}
70 nfcv 2959 . . . . . . . 8 𝑦On
71 nfcv 2959 . . . . . . . . 9 𝑦𝐵
72 nfcv 2959 . . . . . . . . . 10 𝑦𝐴
73 nfcv 2959 . . . . . . . . . 10 𝑦 +𝑜
7472, 73, 69nfov 6914 . . . . . . . . 9 𝑦(𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)})
7571, 74nfss 3802 . . . . . . . 8 𝑦 𝐵 ⊆ (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)})
76 oveq2 6892 . . . . . . . . 9 (𝑦 = {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → (𝐴 +𝑜 𝑦) = (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}))
7776sseq2d 3841 . . . . . . . 8 (𝑦 = {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → (𝐵 ⊆ (𝐴 +𝑜 𝑦) ↔ 𝐵 ⊆ (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)})))
7869, 70, 75, 77elrabf 3566 . . . . . . 7 ( {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ↔ ( {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ On ∧ 𝐵 ⊆ (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)})))
7978simprbi 486 . . . . . 6 ( {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → 𝐵 ⊆ (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}))
8067, 79syl 17 . . . . 5 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → 𝐵 ⊆ (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}))
8165, 80eqssd 3826 . . . 4 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) = 𝐵)
82 oveq2 6892 . . . . . 6 (𝑥 = {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}))
8382eqeq1d 2819 . . . . 5 (𝑥 = {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} → ((𝐴 +𝑜 𝑥) = 𝐵 ↔ (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) = 𝐵))
8483rspcev 3513 . . . 4 (( {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)} ∈ ω ∧ (𝐴 +𝑜 {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +𝑜 𝑦)}) = 𝐵) → ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝐵)
8522, 81, 84syl2anc 575 . . 3 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴𝐵) → ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝐵)
8685ex 399 . 2 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴𝐵 → ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝐵))
87 nnaword1 7956 . . . . 5 ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → 𝐴 ⊆ (𝐴 +𝑜 𝑥))
8887adantlr 697 . . . 4 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑥 ∈ ω) → 𝐴 ⊆ (𝐴 +𝑜 𝑥))
89 sseq2 3835 . . . 4 ((𝐴 +𝑜 𝑥) = 𝐵 → (𝐴 ⊆ (𝐴 +𝑜 𝑥) ↔ 𝐴𝐵))
9088, 89syl5ibcom 236 . . 3 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑥 ∈ ω) → ((𝐴 +𝑜 𝑥) = 𝐵𝐴𝐵))
9190rexlimdva 3230 . 2 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝐵𝐴𝐵))
9286, 91impbid 203 1 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴𝐵 ↔ ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865   = wceq 1637  wcel 2157  wne 2989  wrex 3108  {crab 3111  wss 3780  c0 4127   cint 4680  Ord word 5949  Oncon0 5950  suc csuc 5952  (class class class)co 6884  ωcom 7305   +𝑜 coa 7803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-om 7306  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-oadd 7810
This theorem is referenced by:  nnaordex  7965  unfilem1  8473  hashdom  13406
  Copyright terms: Public domain W3C validator