Theorem oasubex 43292

Description: While subtraction can't be a binary operation on ordinals, for any pair of ordinals there exists an ordinal that can be added to the lessor (or equal) one which will sum to the greater. Theorem 2.19 of [Schloeder] p. 6. (Contributed by RP, 29-Jan-2025.)

Assertion

Ref	Expression
oasubex	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) → ∃𝑐 ∈ On (𝑐 ⊆ 𝐴 ∧ (𝐵 +o 𝑐) = 𝐴))

Distinct variable groups:   𝐴,𝑐   𝐵,𝑐

Proof of Theorem oasubex

Step	Hyp	Ref	Expression
1		simp2 1138	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ On)
2		simp1 1137	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) → 𝐴 ∈ On)
3		simp3 1139	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝐴)
4		oawordex 8603	. . . 4 ⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ On) → (𝐵 ⊆ 𝐴 ↔ ∃𝑐 ∈ On (𝐵 +o 𝑐) = 𝐴))
5	4	biimpa 476	. . 3 ⊢ (((𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ 𝐵 ⊆ 𝐴) → ∃𝑐 ∈ On (𝐵 +o 𝑐) = 𝐴)
6	1, 2, 3, 5	syl21anc 838	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) → ∃𝑐 ∈ On (𝐵 +o 𝑐) = 𝐴)
7		simpr 484	. . . . . . 7 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ∈ On) ∧ (𝐵 +o 𝑐) = 𝐴) → (𝐵 +o 𝑐) = 𝐴)
8		simpl1 1192	. . . . . . . . 9 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ∈ On) → 𝐴 ∈ On)
9		simpl2 1193	. . . . . . . . 9 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ∈ On) → 𝐵 ∈ On)
10		oaword2 8599	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐵 +o 𝐴))
11	8, 9, 10	syl2anc 584	. . . . . . . 8 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ∈ On) → 𝐴 ⊆ (𝐵 +o 𝐴))
12	11	adantr 480	. . . . . . 7 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ∈ On) ∧ (𝐵 +o 𝑐) = 𝐴) → 𝐴 ⊆ (𝐵 +o 𝐴))
13	7, 12	eqsstrd 4037	. . . . . 6 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ∈ On) ∧ (𝐵 +o 𝑐) = 𝐴) → (𝐵 +o 𝑐) ⊆ (𝐵 +o 𝐴))
14		simpr 484	. . . . . . . 8 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ∈ On) → 𝑐 ∈ On)
15		oaword 8595	. . . . . . . 8 ⊢ ((𝑐 ∈ On ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑐 ⊆ 𝐴 ↔ (𝐵 +o 𝑐) ⊆ (𝐵 +o 𝐴)))
16	14, 8, 9, 15	syl3anc 1372	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ∈ On) → (𝑐 ⊆ 𝐴 ↔ (𝐵 +o 𝑐) ⊆ (𝐵 +o 𝐴)))
17	16	adantr 480	. . . . . 6 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ∈ On) ∧ (𝐵 +o 𝑐) = 𝐴) → (𝑐 ⊆ 𝐴 ↔ (𝐵 +o 𝑐) ⊆ (𝐵 +o 𝐴)))
18	13, 17	mpbird 257	. . . . 5 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ∈ On) ∧ (𝐵 +o 𝑐) = 𝐴) → 𝑐 ⊆ 𝐴)
19	18	ex 412	. . . 4 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ∈ On) → ((𝐵 +o 𝑐) = 𝐴 → 𝑐 ⊆ 𝐴))
20	19	ancrd 551	. . 3 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ∈ On) → ((𝐵 +o 𝑐) = 𝐴 → (𝑐 ⊆ 𝐴 ∧ (𝐵 +o 𝑐) = 𝐴)))
21	20	reximdva 3168	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) → (∃𝑐 ∈ On (𝐵 +o 𝑐) = 𝐴 → ∃𝑐 ∈ On (𝑐 ⊆ 𝐴 ∧ (𝐵 +o 𝑐) = 𝐴)))
22	6, 21	mpd 15	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) → ∃𝑐 ∈ On (𝑐 ⊆ 𝐴 ∧ (𝐵 +o 𝑐) = 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1539   ∈ wcel 2108  ∃wrex 3070   ⊆ wss 3966  Oncon0 6392  (class class class)co 7438   +_o coa 8511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5288  ax-sep 5305  ax-nul 5315  ax-pr 5441  ax-un 7761

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3483  df-sbc 3795  df-csb 3912  df-dif 3969  df-un 3971  df-in 3973  df-ss 3983  df-pss 3986  df-nul 4343  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4916  df-int 4955  df-iun 5001  df-br 5152  df-opab 5214  df-mpt 5235  df-tr 5269  df-id 5587  df-eprel 5593  df-po 5601  df-so 5602  df-fr 5645  df-we 5647  df-xp 5699  df-rel 5700  df-cnv 5701  df-co 5702  df-dm 5703  df-rn 5704  df-res 5705  df-ima 5706  df-pred 6329  df-ord 6395  df-on 6396  df-lim 6397  df-suc 6398  df-iota 6522  df-fun 6571  df-fn 6572  df-f 6573  df-f1 6574  df-fo 6575  df-f1o 6576  df-fv 6577  df-ov 7441  df-oprab 7442  df-mpo 7443  df-om 7895  df-2nd 8023  df-frecs 8314  df-wrecs 8345  df-recs 8419  df-rdg 8458  df-oadd 8518

This theorem is referenced by: (None)