Theorem oaun3lem1 42109

Description: The class of all ordinal sums of elements from two ordinals is ordinal. Lemma for oaun3 42117. (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 1917	. . . . . 6 ⊢ Ⅎ𝑎(𝐴 ∈ On ∧ 𝐵 ∈ On)
2		nfcv 2903	. . . . . . 7 ⊢ Ⅎ𝑎𝑦
3		nfre1 3282	. . . . . . . 8 ⊢ Ⅎ𝑎∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
4	3	nfsab 2722	. . . . . . 7 ⊢ Ⅎ𝑎 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
5	2, 4	nfralw 3308	. . . . . 6 ⊢ Ⅎ𝑎∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
6		nfv 1917	. . . . . . . 8 ⊢ Ⅎ𝑏((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴)
7		nfcv 2903	. . . . . . . . 9 ⊢ Ⅎ𝑏𝑦
8		nfcv 2903	. . . . . . . . . . 11 ⊢ Ⅎ𝑏𝐴
9		nfre1 3282	. . . . . . . . . . 11 ⊢ Ⅎ𝑏∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
10	8, 9	nfrexw 3310	. . . . . . . . . 10 ⊢ Ⅎ𝑏∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
11	10	nfsab 2722	. . . . . . . . 9 ⊢ Ⅎ𝑏 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
12	7, 11	nfralw 3308	. . . . . . . 8 ⊢ Ⅎ𝑏∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
13		simp-4l 781	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → 𝐴 ∈ On)
14		simplrl 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑎 ∈ 𝐴)
15	14	anim1ci 616	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → (𝑧 ∈ 𝑎 ∧ 𝑎 ∈ 𝐴))
16		ontr1 6407	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ On → ((𝑧 ∈ 𝑎 ∧ 𝑎 ∈ 𝐴) → 𝑧 ∈ 𝐴))
17	13, 15, 16	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → 𝑧 ∈ 𝐴)
18		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐵 ∈ On)
19		ne0i 4333	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ 𝐵 → 𝐵 ≠ ∅)
20	19	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐵 ≠ ∅)
21		on0eln0 6417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅))
22	21	biimpar 478	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ On ∧ 𝐵 ≠ ∅) → ∅ ∈ 𝐵)
23	18, 20, 22	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ∅ ∈ 𝐵)
24		onelon 6386	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ On)
25	24	ad2ant2r 745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ On)
26		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
27		onelon 6386	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 ∈ On ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ On)
28	18, 26, 27	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ On)
29		oacl 8531	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +o 𝑏) ∈ On)
30	25, 28, 29	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ∈ On)
31		onelon 6386	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 +o 𝑏) ∈ On ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ On)
32	30, 31	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ On)
33		oa0 8512	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ On → (𝑧 +o ∅) = 𝑧)
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑧 +o ∅) = 𝑧)
35	34	eqcomd 2738	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 = (𝑧 +o ∅))
36		oveq2 7413	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → (𝑧 +o 𝑦) = (𝑧 +o ∅))
37	36	rspceeqv 3632	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ 𝐵 ∧ 𝑧 = (𝑧 +o ∅)) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
38	23, 35, 37	syl2an2r 683	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
39	38	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
40		oveq1 7412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑧 → (𝑤 +o 𝑦) = (𝑧 +o 𝑦))
41	40	eqeq2d 2743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑧 → (𝑧 = (𝑤 +o 𝑦) ↔ 𝑧 = (𝑧 +o 𝑦)))
42	41	rexbidv 3178	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑧 → (∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦) ↔ ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦)))
43	42	rspcev 3612	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦)) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
44	17, 39, 43	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
45	18	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝐵 ∈ On)
46	25, 45	jca 512	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 ∈ On ∧ 𝐵 ∈ On))
47	46	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑎 ∈ On ∧ 𝐵 ∈ On))
48		oacl 8531	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ On ∧ 𝐵 ∈ On) → (𝑎 +o 𝐵) ∈ On)
49	25, 45, 48	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝐵) ∈ On)
50		eloni 6371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 +o 𝑏) ∈ On → Ord (𝑎 +o 𝑏))
51		eloni 6371	. . . . . . . . . . . . . . . . . . . . . . 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 512	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝐵 ∈ On ∧ 𝑎 ∈ On))
55	26	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵)
56		oaordi 8542	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ On ∧ 𝑎 ∈ On) → (𝑏 ∈ 𝐵 → (𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵)))
57	54, 55, 56	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵))
58		ordelpss 6389	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)) → ((𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵) ↔ (𝑎 +o 𝑏) ⊊ (𝑎 +o 𝐵)))
59	58	biimpd 228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)) → ((𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵) → (𝑎 +o 𝑏) ⊊ (𝑎 +o 𝐵)))
60	53, 57, 59	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ⊊ (𝑎 +o 𝐵))
61	60	pssssd 4096	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ⊆ (𝑎 +o 𝐵))
62	61	sselda 3981	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ (𝑎 +o 𝐵))
63	62	anim1ci 616	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → (𝑎 ⊆ 𝑧 ∧ 𝑧 ∈ (𝑎 +o 𝐵)))
64		oawordex2 42061	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ⊆ 𝑧 ∧ 𝑧 ∈ (𝑎 +o 𝐵))) → ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧)
65	47, 63, 64	syl2an2r 683	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧)
66		oveq1 7412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑎 → (𝑤 +o 𝑦) = (𝑎 +o 𝑦))
67	66	eqeq2d 2743	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑎 → (𝑧 = (𝑤 +o 𝑦) ↔ 𝑧 = (𝑎 +o 𝑦)))
68		eqcom 2739	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑎 +o 𝑦) ↔ (𝑎 +o 𝑦) = 𝑧)
69	67, 68	bitrdi 286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑎 → (𝑧 = (𝑤 +o 𝑦) ↔ (𝑎 +o 𝑦) = 𝑧))
70	69	rexbidv 3178	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → (∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦) ↔ ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧))
71	70	rspcev 3612	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
72	14, 65, 71	syl2an2r 683	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
73		eloni 6371	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ On → Ord 𝑧)
74	32, 73	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → Ord 𝑧)
75		eloni 6371	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ On → Ord 𝑎)
76	25, 75	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → Ord 𝑎)
77	76	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → Ord 𝑎)
78		ordtri2or 6459	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝑧 ∧ Ord 𝑎) → (𝑧 ∈ 𝑎 ∨ 𝑎 ⊆ 𝑧))
79	74, 77, 78	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑧 ∈ 𝑎 ∨ 𝑎 ⊆ 𝑧))
80	44, 72, 79	mpjaodan 957	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
81		vex 3478	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
82		eqeq1 2736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → (𝑥 = (𝑎 +o 𝑏) ↔ 𝑧 = (𝑎 +o 𝑏)))
83	82	2rexbidv 3219	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏)))
84		oveq1 7412	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑤 → (𝑎 +o 𝑏) = (𝑤 +o 𝑏))
85	84	eqeq2d 2743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑤 → (𝑧 = (𝑎 +o 𝑏) ↔ 𝑧 = (𝑤 +o 𝑏)))
86		oveq2 7413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑦 → (𝑤 +o 𝑏) = (𝑤 +o 𝑦))
87	86	eqeq2d 2743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑦 → (𝑧 = (𝑤 +o 𝑏) ↔ 𝑧 = (𝑤 +o 𝑦)))
88	85, 87	cbvrex2vw 3239	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏) ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
89	83, 88	bitrdi 286	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦)))
90	81, 89	elab 3667	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
91	80, 90	sylibr 233	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
92	91	ralrimiva 3146	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ∀𝑧 ∈ (𝑎 +o 𝑏)𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
93	92	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → ∀𝑧 ∈ (𝑎 +o 𝑏)𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
94		simpr 485	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → 𝑦 = (𝑎 +o 𝑏))
95	94	raleqdv 3325	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → (∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∀𝑧 ∈ (𝑎 +o 𝑏)𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
96	93, 95	mpbird 256	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
97	96	exp31 420	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
98	97	expdimp 453	. . . . . . . 8 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴) → (𝑏 ∈ 𝐵 → (𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
99	6, 12, 98	rexlimd 3263	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
100	99	ex 413	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑎 ∈ 𝐴 → (∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
101	1, 5, 100	rexlimd 3263	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
102	101	alrimiv 1930	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑦(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
103		eqeq1 2736	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 = (𝑎 +o 𝑏) ↔ 𝑦 = (𝑎 +o 𝑏)))
104	103	2rexbidv 3219	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏)))
105	104	ralab 3686	. . . 4 ⊢ (∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∀𝑦(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
106	102, 105	sylibr 233	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
107		dftr5 5268	. . 3 ⊢ (Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
108	106, 107	sylibr 233	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
109		simpr 485	. . . . . . 7 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → 𝑥 = (𝑎 +o 𝑏))
110	30	adantr 481	. . . . . . 7 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → (𝑎 +o 𝑏) ∈ On)
111	109, 110	eqeltrd 2833	. . . . . 6 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → 𝑥 ∈ On)
112	111	exp31 420	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑥 = (𝑎 +o 𝑏) → 𝑥 ∈ On)))
113	112	rexlimdvv 3210	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) → 𝑥 ∈ On))
114	113	abssdv 4064	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ On)
115		epweon 7758	. . 3 ⊢ E We On
116		wess 5662	. . 3 ⊢ ({𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ On → ( E We On → E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
117	114, 115, 116	mpisyl 21	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
118		df-ord 6364	. 2 ⊢ (Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ (Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ∧ E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
119	108, 117, 118	sylanbrc 583	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 845  ∀wal 1539   = wceq 1541   ∈ wcel 2106  {cab 2709   ≠ wne 2940  ∀wral 3061  ∃wrex 3070   ⊆ wss 3947   ⊊ wpss 3948  ∅c0 4321  Tr wtr 5264   E cep 5578   We wwe 5629  Ord word 6360  Oncon0 6361  (class class class)co 7405   +_o coa 8459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-oadd 8466

This theorem is referenced by:  oaun3lem3  42111