Theorem oaun3lem1 43832

Description: The class of all ordinal sums of elements from two ordinals is ordinal. Lemma for oaun3 43840. (Contributed by RP, 13-Feb-2025.)

Assertion

Ref	Expression
oaun3lem1	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})

Distinct variable groups:   𝐴,𝑎,𝑏,𝑥   𝐵,𝑎,𝑏,𝑥

Proof of Theorem oaun3lem1

Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1922	. . . . . 6 ⊢ Ⅎ𝑎(𝐴 ∈ On ∧ 𝐵 ∈ On)
2		nfcv 2903	. . . . . . 7 ⊢ Ⅎ𝑎𝑦
3		nfre1 3266	. . . . . . . 8 ⊢ Ⅎ𝑎∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
4	3	nfsab 2731	. . . . . . 7 ⊢ Ⅎ𝑎 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
5	2, 4	nfralw 3288	. . . . . 6 ⊢ Ⅎ𝑎∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
6		nfv 1922	. . . . . . . 8 ⊢ Ⅎ𝑏((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴)
7		nfcv 2903	. . . . . . . . 9 ⊢ Ⅎ𝑏𝑦
8		nfcv 2903	. . . . . . . . . . 11 ⊢ Ⅎ𝑏𝐴
9		nfre1 3266	. . . . . . . . . . 11 ⊢ Ⅎ𝑏∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
10	8, 9	nfrexw 3289	. . . . . . . . . 10 ⊢ Ⅎ𝑏∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
11	10	nfsab 2731	. . . . . . . . 9 ⊢ Ⅎ𝑏 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
12	7, 11	nfralw 3288	. . . . . . . 8 ⊢ Ⅎ𝑏∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
13		simp-4l 789	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → 𝐴 ∈ On)
14		simplrl 783	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑎 ∈ 𝐴)
15	14	anim1ci 623	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → (𝑧 ∈ 𝑎 ∧ 𝑎 ∈ 𝐴))
16		ontr1 6360	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ On → ((𝑧 ∈ 𝑎 ∧ 𝑎 ∈ 𝐴) → 𝑧 ∈ 𝐴))
17	13, 15, 16	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → 𝑧 ∈ 𝐴)
18		simpr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐵 ∈ On)
19		ne0i 4271	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ 𝐵 → 𝐵 ≠ ∅)
20	19	adantl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐵 ≠ ∅)
21		on0eln0 6370	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅))
22	21	biimpar 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ On ∧ 𝐵 ≠ ∅) → ∅ ∈ 𝐵)
23	18, 20, 22	syl2an 603	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ∅ ∈ 𝐵)
24		onelon 6338	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ On)
25	24	ad2ant2r 754	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ On)
26		simpr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
27		onelon 6338	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 ∈ On ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ On)
28	18, 26, 27	syl2an 603	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ On)
29		oacl 8464	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +o 𝑏) ∈ On)
30	25, 28, 29	syl2anc 591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ∈ On)
31		onelon 6338	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 +o 𝑏) ∈ On ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ On)
32	30, 31	sylan 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ On)
33		oa0 8445	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ On → (𝑧 +o ∅) = 𝑧)
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑧 +o ∅) = 𝑧)
35	34	eqcomd 2747	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 = (𝑧 +o ∅))
36		oveq2 7367	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → (𝑧 +o 𝑦) = (𝑧 +o ∅))
37	36	rspceeqv 3584	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ 𝐵 ∧ 𝑧 = (𝑧 +o ∅)) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
38	23, 35, 37	syl2an2r 692	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
39	38	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
40		oveq1 7366	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑧 → (𝑤 +o 𝑦) = (𝑧 +o 𝑦))
41	40	eqeq2d 2752	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑧 → (𝑧 = (𝑤 +o 𝑦) ↔ 𝑧 = (𝑧 +o 𝑦)))
42	41	rexbidv 3165	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑧 → (∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦) ↔ ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦)))
43	42	rspcev 3561	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦)) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
44	17, 39, 43	syl2anc 591	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
45	18	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝐵 ∈ On)
46	25, 45	jca 517	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 ∈ On ∧ 𝐵 ∈ On))
47	46	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑎 ∈ On ∧ 𝐵 ∈ On))
48		oacl 8464	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ On ∧ 𝐵 ∈ On) → (𝑎 +o 𝐵) ∈ On)
49	25, 45, 48	syl2anc 591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝐵) ∈ On)
50		eloni 6323	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 +o 𝑏) ∈ On → Ord (𝑎 +o 𝑏))
51		eloni 6323	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 +o 𝐵) ∈ On → Ord (𝑎 +o 𝐵))
52	50, 51	anim12i 620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 +o 𝑏) ∈ On ∧ (𝑎 +o 𝐵) ∈ On) → (Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)))
53	30, 49, 52	syl2anc 591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)))
54	45, 25	jca 517	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝐵 ∈ On ∧ 𝑎 ∈ On))
55	26	adantl 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵)
56		oaordi 8475	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ On ∧ 𝑎 ∈ On) → (𝑏 ∈ 𝐵 → (𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵)))
57	54, 55, 56	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵))
58		ordelpss 6341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)) → ((𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵) ↔ (𝑎 +o 𝑏) ⊊ (𝑎 +o 𝐵)))
59	58	biimpd 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)) → ((𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵) → (𝑎 +o 𝑏) ⊊ (𝑎 +o 𝐵)))
60	53, 57, 59	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ⊊ (𝑎 +o 𝐵))
61	60	pssssd 4033	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ⊆ (𝑎 +o 𝐵))
62	61	sselda 3916	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ (𝑎 +o 𝐵))
63	62	anim1ci 623	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → (𝑎 ⊆ 𝑧 ∧ 𝑧 ∈ (𝑎 +o 𝐵)))
64		oawordex2 43784	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ⊆ 𝑧 ∧ 𝑧 ∈ (𝑎 +o 𝐵))) → ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧)
65	47, 63, 64	syl2an2r 692	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧)
66		oveq1 7366	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑎 → (𝑤 +o 𝑦) = (𝑎 +o 𝑦))
67	66	eqeq2d 2752	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑎 → (𝑧 = (𝑤 +o 𝑦) ↔ 𝑧 = (𝑎 +o 𝑦)))
68		eqcom 2748	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑎 +o 𝑦) ↔ (𝑎 +o 𝑦) = 𝑧)
69	67, 68	bitrdi 289	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑎 → (𝑧 = (𝑤 +o 𝑦) ↔ (𝑎 +o 𝑦) = 𝑧))
70	69	rexbidv 3165	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → (∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦) ↔ ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧))
71	70	rspcev 3561	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
72	14, 65, 71	syl2an2r 692	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
73		eloni 6323	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ On → Ord 𝑧)
74	32, 73	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → Ord 𝑧)
75		eloni 6323	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ On → Ord 𝑎)
76	25, 75	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → Ord 𝑎)
77	76	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → Ord 𝑎)
78		ordtri2or 6413	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝑧 ∧ Ord 𝑎) → (𝑧 ∈ 𝑎 ∨ 𝑎 ⊆ 𝑧))
79	74, 77, 78	syl2anc 591	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑧 ∈ 𝑎 ∨ 𝑎 ⊆ 𝑧))
80	44, 72, 79	mpjaodan 967	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
81		vex 3437	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
82		eqeq1 2745	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → (𝑥 = (𝑎 +o 𝑏) ↔ 𝑧 = (𝑎 +o 𝑏)))
83	82	2rexbidv 3206	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏)))
84		oveq1 7366	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑤 → (𝑎 +o 𝑏) = (𝑤 +o 𝑏))
85	84	eqeq2d 2752	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑤 → (𝑧 = (𝑎 +o 𝑏) ↔ 𝑧 = (𝑤 +o 𝑏)))
86		oveq2 7367	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑦 → (𝑤 +o 𝑏) = (𝑤 +o 𝑦))
87	86	eqeq2d 2752	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑦 → (𝑧 = (𝑤 +o 𝑏) ↔ 𝑧 = (𝑤 +o 𝑦)))
88	85, 87	cbvrex2vw 3224	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏) ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
89	83, 88	bitrdi 289	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦)))
90	81, 89	elab 3618	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
91	80, 90	sylibr 236	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
92	91	ralrimiva 3133	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ∀𝑧 ∈ (𝑎 +o 𝑏)𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
93	92	adantr 482	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → ∀𝑧 ∈ (𝑎 +o 𝑏)𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
94		simpr 486	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → 𝑦 = (𝑎 +o 𝑏))
95	93, 94	raleqtrrdv 3303	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
96	95	exp31 421	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
97	96	expdimp 454	. . . . . . . 8 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴) → (𝑏 ∈ 𝐵 → (𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
98	6, 12, 97	rexlimd 3248	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
99	98	ex 414	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑎 ∈ 𝐴 → (∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
100	1, 5, 99	rexlimd 3248	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
101	100	alrimiv 1935	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑦(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
102		eqeq1 2745	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 = (𝑎 +o 𝑏) ↔ 𝑦 = (𝑎 +o 𝑏)))
103	102	2rexbidv 3206	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏)))
104	103	ralab 3635	. . . 4 ⊢ (∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∀𝑦(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
105	101, 104	sylibr 236	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
106		dftr5 5185	. . 3 ⊢ (Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
107	105, 106	sylibr 236	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
108		simpr 486	. . . . . . 7 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → 𝑥 = (𝑎 +o 𝑏))
109	30	adantr 482	. . . . . . 7 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → (𝑎 +o 𝑏) ∈ On)
110	108, 109	eqeltrd 2841	. . . . . 6 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → 𝑥 ∈ On)
111	110	exp31 421	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑥 = (𝑎 +o 𝑏) → 𝑥 ∈ On)))
112	111	rexlimdvv 3197	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) → 𝑥 ∈ On))
113	112	abssdv 4000	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ On)
114		epweon 7721	. . 3 ⊢ E We On
115		wess 5606	. . 3 ⊢ ({𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ On → ( E We On → E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
116	113, 114, 115	mpisyl 21	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
117		df-ord 6316	. 2 ⊢ (Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ (Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ∧ E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
118	107, 116, 117	sylanbrc 590	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})

Syntax hints:   → wi 4   ∧ wa 397   ∨ wo 854  ∀wal 1546   = wceq 1548   ∈ wcel 2121  {cab 2719   ≠ wne 2936  ∀wral 3055  ∃wrex 3065   ⊆ wss 3884   ⊊ wpss 3885  ∅c0 4263  Tr wtr 5181   E cep 5519   We wwe 5572  Ord word 6312  Oncon0 6313  (class class class)co 7359   +_o coa 8396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5201  ax-sep 5220  ax-nul 5230  ax-pr 5364  ax-un 7681

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3725  df-csb 3833  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3904  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-int 4880  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-ov 7362  df-oprab 7363  df-mpo 7364  df-om 7810  df-2nd 7934  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8343  df-oadd 8403

This theorem is referenced by:  oaun3lem3  43834