Theorem oaun3lem1 43387

Description: The class of all ordinal sums of elements from two ordinals is ordinal. Lemma for oaun3 43395. (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 1914	. . . . . 6 ⊢ Ⅎ𝑎(𝐴 ∈ On ∧ 𝐵 ∈ On)
2		nfcv 2905	. . . . . . 7 ⊢ Ⅎ𝑎𝑦
3		nfre1 3285	. . . . . . . 8 ⊢ Ⅎ𝑎∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
4	3	nfsab 2727	. . . . . . 7 ⊢ Ⅎ𝑎 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
5	2, 4	nfralw 3311	. . . . . 6 ⊢ Ⅎ𝑎∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
6		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑏((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴)
7		nfcv 2905	. . . . . . . . 9 ⊢ Ⅎ𝑏𝑦
8		nfcv 2905	. . . . . . . . . . 11 ⊢ Ⅎ𝑏𝐴
9		nfre1 3285	. . . . . . . . . . 11 ⊢ Ⅎ𝑏∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
10	8, 9	nfrexw 3313	. . . . . . . . . 10 ⊢ Ⅎ𝑏∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
11	10	nfsab 2727	. . . . . . . . 9 ⊢ Ⅎ𝑏 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
12	7, 11	nfralw 3311	. . . . . . . 8 ⊢ Ⅎ𝑏∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
13		simp-4l 783	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → 𝐴 ∈ On)
14		simplrl 777	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑎 ∈ 𝐴)
15	14	anim1ci 616	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → (𝑧 ∈ 𝑎 ∧ 𝑎 ∈ 𝐴))
16		ontr1 6430	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ On → ((𝑧 ∈ 𝑎 ∧ 𝑎 ∈ 𝐴) → 𝑧 ∈ 𝐴))
17	13, 15, 16	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → 𝑧 ∈ 𝐴)
18		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐵 ∈ On)
19		ne0i 4341	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ 𝐵 → 𝐵 ≠ ∅)
20	19	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐵 ≠ ∅)
21		on0eln0 6440	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅))
22	21	biimpar 477	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ On ∧ 𝐵 ≠ ∅) → ∅ ∈ 𝐵)
23	18, 20, 22	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ∅ ∈ 𝐵)
24		onelon 6409	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ On)
25	24	ad2ant2r 747	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ On)
26		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
27		onelon 6409	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 ∈ On ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ On)
28	18, 26, 27	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ On)
29		oacl 8573	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +o 𝑏) ∈ On)
30	25, 28, 29	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ∈ On)
31		onelon 6409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 +o 𝑏) ∈ On ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ On)
32	30, 31	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ On)
33		oa0 8554	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ On → (𝑧 +o ∅) = 𝑧)
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑧 +o ∅) = 𝑧)
35	34	eqcomd 2743	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 = (𝑧 +o ∅))
36		oveq2 7439	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → (𝑧 +o 𝑦) = (𝑧 +o ∅))
37	36	rspceeqv 3645	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ 𝐵 ∧ 𝑧 = (𝑧 +o ∅)) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
38	23, 35, 37	syl2an2r 685	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
39	38	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
40		oveq1 7438	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑧 → (𝑤 +o 𝑦) = (𝑧 +o 𝑦))
41	40	eqeq2d 2748	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑧 → (𝑧 = (𝑤 +o 𝑦) ↔ 𝑧 = (𝑧 +o 𝑦)))
42	41	rexbidv 3179	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑧 → (∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦) ↔ ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦)))
43	42	rspcev 3622	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦)) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
44	17, 39, 43	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
45	18	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝐵 ∈ On)
46	25, 45	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 ∈ On ∧ 𝐵 ∈ On))
47	46	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑎 ∈ On ∧ 𝐵 ∈ On))
48		oacl 8573	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ On ∧ 𝐵 ∈ On) → (𝑎 +o 𝐵) ∈ On)
49	25, 45, 48	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝐵) ∈ On)
50		eloni 6394	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 +o 𝑏) ∈ On → Ord (𝑎 +o 𝑏))
51		eloni 6394	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 +o 𝐵) ∈ On → Ord (𝑎 +o 𝐵))
52	50, 51	anim12i 613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 +o 𝑏) ∈ On ∧ (𝑎 +o 𝐵) ∈ On) → (Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)))
53	30, 49, 52	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)))
54	45, 25	jca 511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝐵 ∈ On ∧ 𝑎 ∈ On))
55	26	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵)
56		oaordi 8584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ On ∧ 𝑎 ∈ On) → (𝑏 ∈ 𝐵 → (𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵)))
57	54, 55, 56	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵))
58		ordelpss 6412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)) → ((𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵) ↔ (𝑎 +o 𝑏) ⊊ (𝑎 +o 𝐵)))
59	58	biimpd 229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)) → ((𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵) → (𝑎 +o 𝑏) ⊊ (𝑎 +o 𝐵)))
60	53, 57, 59	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ⊊ (𝑎 +o 𝐵))
61	60	pssssd 4100	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ⊆ (𝑎 +o 𝐵))
62	61	sselda 3983	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ (𝑎 +o 𝐵))
63	62	anim1ci 616	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → (𝑎 ⊆ 𝑧 ∧ 𝑧 ∈ (𝑎 +o 𝐵)))
64		oawordex2 43339	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ⊆ 𝑧 ∧ 𝑧 ∈ (𝑎 +o 𝐵))) → ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧)
65	47, 63, 64	syl2an2r 685	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧)
66		oveq1 7438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑎 → (𝑤 +o 𝑦) = (𝑎 +o 𝑦))
67	66	eqeq2d 2748	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑎 → (𝑧 = (𝑤 +o 𝑦) ↔ 𝑧 = (𝑎 +o 𝑦)))
68		eqcom 2744	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑎 +o 𝑦) ↔ (𝑎 +o 𝑦) = 𝑧)
69	67, 68	bitrdi 287	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑎 → (𝑧 = (𝑤 +o 𝑦) ↔ (𝑎 +o 𝑦) = 𝑧))
70	69	rexbidv 3179	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → (∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦) ↔ ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧))
71	70	rspcev 3622	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
72	14, 65, 71	syl2an2r 685	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
73		eloni 6394	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ On → Ord 𝑧)
74	32, 73	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → Ord 𝑧)
75		eloni 6394	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ On → Ord 𝑎)
76	25, 75	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → Ord 𝑎)
77	76	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → Ord 𝑎)
78		ordtri2or 6482	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝑧 ∧ Ord 𝑎) → (𝑧 ∈ 𝑎 ∨ 𝑎 ⊆ 𝑧))
79	74, 77, 78	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑧 ∈ 𝑎 ∨ 𝑎 ⊆ 𝑧))
80	44, 72, 79	mpjaodan 961	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
81		vex 3484	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
82		eqeq1 2741	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → (𝑥 = (𝑎 +o 𝑏) ↔ 𝑧 = (𝑎 +o 𝑏)))
83	82	2rexbidv 3222	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏)))
84		oveq1 7438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑤 → (𝑎 +o 𝑏) = (𝑤 +o 𝑏))
85	84	eqeq2d 2748	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑤 → (𝑧 = (𝑎 +o 𝑏) ↔ 𝑧 = (𝑤 +o 𝑏)))
86		oveq2 7439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑦 → (𝑤 +o 𝑏) = (𝑤 +o 𝑦))
87	86	eqeq2d 2748	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑦 → (𝑧 = (𝑤 +o 𝑏) ↔ 𝑧 = (𝑤 +o 𝑦)))
88	85, 87	cbvrex2vw 3242	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏) ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
89	83, 88	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦)))
90	81, 89	elab 3679	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
91	80, 90	sylibr 234	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
92	91	ralrimiva 3146	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ∀𝑧 ∈ (𝑎 +o 𝑏)𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
93	92	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → ∀𝑧 ∈ (𝑎 +o 𝑏)𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
94		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → 𝑦 = (𝑎 +o 𝑏))
95	93, 94	raleqtrrdv 3330	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
96	95	exp31 419	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
97	96	expdimp 452	. . . . . . . 8 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴) → (𝑏 ∈ 𝐵 → (𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
98	6, 12, 97	rexlimd 3266	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
99	98	ex 412	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑎 ∈ 𝐴 → (∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
100	1, 5, 99	rexlimd 3266	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
101	100	alrimiv 1927	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑦(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
102		eqeq1 2741	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 = (𝑎 +o 𝑏) ↔ 𝑦 = (𝑎 +o 𝑏)))
103	102	2rexbidv 3222	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏)))
104	103	ralab 3697	. . . 4 ⊢ (∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∀𝑦(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
105	101, 104	sylibr 234	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
106		dftr5 5263	. . 3 ⊢ (Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
107	105, 106	sylibr 234	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
108		simpr 484	. . . . . . 7 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → 𝑥 = (𝑎 +o 𝑏))
109	30	adantr 480	. . . . . . 7 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → (𝑎 +o 𝑏) ∈ On)
110	108, 109	eqeltrd 2841	. . . . . 6 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → 𝑥 ∈ On)
111	110	exp31 419	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑥 = (𝑎 +o 𝑏) → 𝑥 ∈ On)))
112	111	rexlimdvv 3212	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) → 𝑥 ∈ On))
113	112	abssdv 4068	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ On)
114		epweon 7795	. . 3 ⊢ E We On
115		wess 5671	. . 3 ⊢ ({𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ On → ( E We On → E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
116	113, 114, 115	mpisyl 21	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
117		df-ord 6387	. 2 ⊢ (Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ (Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ∧ E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
118	107, 116, 117	sylanbrc 583	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848  ∀wal 1538   = wceq 1540   ∈ wcel 2108  {cab 2714   ≠ wne 2940  ∀wral 3061  ∃wrex 3070   ⊆ wss 3951   ⊊ wpss 3952  ∅c0 4333  Tr wtr 5259   E cep 5583   We wwe 5636  Ord word 6383  Oncon0 6384  (class class class)co 7431   +_o coa 8503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  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 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  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 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-oadd 8510

This theorem is referenced by:  oaun3lem3  43389