Theorem oaun3lem1 43956

Description: The class of all ordinal sums of elements from two ordinals is ordinal. Lemma for oaun3 43964. (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 1936	. . . . . 6 ⊢ Ⅎ𝑎(𝐴 ∈ On ∧ 𝐵 ∈ On)
2		nfcv 2926	. . . . . . 7 ⊢ Ⅎ𝑎𝑦
3		nfre1 3289	. . . . . . . 8 ⊢ Ⅎ𝑎∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
4	3	nfsab 2754	. . . . . . 7 ⊢ Ⅎ𝑎 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
5	2, 4	nfralw 3311	. . . . . 6 ⊢ Ⅎ𝑎∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
6		nfv 1936	. . . . . . . 8 ⊢ Ⅎ𝑏((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴)
7		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑏𝑦
8		nfcv 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑏𝐴
9		nfre1 3289	. . . . . . . . . . 11 ⊢ Ⅎ𝑏∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
10	8, 9	nfrexw 3312	. . . . . . . . . 10 ⊢ Ⅎ𝑏∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
11	10	nfsab 2754	. . . . . . . . 9 ⊢ Ⅎ𝑏 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
12	7, 11	nfralw 3311	. . . . . . . 8 ⊢ Ⅎ𝑏∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
13		simp-4l 792	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → 𝐴 ∈ On)
14		simplrl 786	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑎 ∈ 𝐴)
15	14	anim1ci 625	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → (𝑧 ∈ 𝑎 ∧ 𝑎 ∈ 𝐴))
16		ontr1 6395	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ On → ((𝑧 ∈ 𝑎 ∧ 𝑎 ∈ 𝐴) → 𝑧 ∈ 𝐴))
17	13, 15, 16	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → 𝑧 ∈ 𝐴)
18		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐵 ∈ On)
19		ne0i 4295	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ 𝐵 → 𝐵 ≠ ∅)
20	19	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐵 ≠ ∅)
21		on0eln0 6405	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅))
22	21	biimpar 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ On ∧ 𝐵 ≠ ∅) → ∅ ∈ 𝐵)
23	18, 20, 22	syl2an 605	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ∅ ∈ 𝐵)
24		onelon 6373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ On)
25	24	ad2ant2r 757	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ On)
26		simpr 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
27		onelon 6373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 ∈ On ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ On)
28	18, 26, 27	syl2an 605	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ On)
29		oacl 8506	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +o 𝑏) ∈ On)
30	25, 28, 29	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ∈ On)
31		onelon 6373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 +o 𝑏) ∈ On ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ On)
32	30, 31	sylan 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ On)
33		oa0 8487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ On → (𝑧 +o ∅) = 𝑧)
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑧 +o ∅) = 𝑧)
35	34	eqcomd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 = (𝑧 +o ∅))
36		oveq2 7406	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → (𝑧 +o 𝑦) = (𝑧 +o ∅))
37	36	rspceeqv 3606	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ 𝐵 ∧ 𝑧 = (𝑧 +o ∅)) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
38	23, 35, 37	syl2an2r 695	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
39	38	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
40		oveq1 7405	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑧 → (𝑤 +o 𝑦) = (𝑧 +o 𝑦))
41	40	eqeq2d 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑧 → (𝑧 = (𝑤 +o 𝑦) ↔ 𝑧 = (𝑧 +o 𝑦)))
42	41	rexbidv 3188	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑧 → (∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦) ↔ ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦)))
43	42	rspcev 3583	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦)) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
44	17, 39, 43	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
45	18	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝐵 ∈ On)
46	25, 45	jca 519	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 ∈ On ∧ 𝐵 ∈ On))
47	46	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑎 ∈ On ∧ 𝐵 ∈ On))
48		oacl 8506	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ On ∧ 𝐵 ∈ On) → (𝑎 +o 𝐵) ∈ On)
49	25, 45, 48	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝐵) ∈ On)
50		eloni 6358	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 +o 𝑏) ∈ On → Ord (𝑎 +o 𝑏))
51		eloni 6358	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 +o 𝐵) ∈ On → Ord (𝑎 +o 𝐵))
52	50, 51	anim12i 622	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 +o 𝑏) ∈ On ∧ (𝑎 +o 𝐵) ∈ On) → (Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)))
53	30, 49, 52	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)))
54	45, 25	jca 519	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝐵 ∈ On ∧ 𝑎 ∈ On))
55	26	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵)
56		oaordi 8517	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ On ∧ 𝑎 ∈ On) → (𝑏 ∈ 𝐵 → (𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵)))
57	54, 55, 56	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵))
58		ordelpss 6376	. . . . . . . . . . . . . . . . . . . . . 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 4055	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ⊆ (𝑎 +o 𝐵))
62	61	sselda 3938	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ (𝑎 +o 𝐵))
63	62	anim1ci 625	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → (𝑎 ⊆ 𝑧 ∧ 𝑧 ∈ (𝑎 +o 𝐵)))
64		oawordex2 43908	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ⊆ 𝑧 ∧ 𝑧 ∈ (𝑎 +o 𝐵))) → ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧)
65	47, 63, 64	syl2an2r 695	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧)
66		oveq1 7405	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑎 → (𝑤 +o 𝑦) = (𝑎 +o 𝑦))
67	66	eqeq2d 2775	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑎 → (𝑧 = (𝑤 +o 𝑦) ↔ 𝑧 = (𝑎 +o 𝑦)))
68		eqcom 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑎 +o 𝑦) ↔ (𝑎 +o 𝑦) = 𝑧)
69	67, 68	bitrdi 289	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑎 → (𝑧 = (𝑤 +o 𝑦) ↔ (𝑎 +o 𝑦) = 𝑧))
70	69	rexbidv 3188	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → (∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦) ↔ ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧))
71	70	rspcev 3583	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
72	14, 65, 71	syl2an2r 695	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
73		eloni 6358	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ On → Ord 𝑧)
74	32, 73	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → Ord 𝑧)
75		eloni 6358	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ On → Ord 𝑎)
76	25, 75	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → Ord 𝑎)
77	76	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → Ord 𝑎)
78		ordtri2or 6448	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝑧 ∧ Ord 𝑎) → (𝑧 ∈ 𝑎 ∨ 𝑎 ⊆ 𝑧))
79	74, 77, 78	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑧 ∈ 𝑎 ∨ 𝑎 ⊆ 𝑧))
80	44, 72, 79	mpjaodan 971	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
81		vex 3460	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
82		eqeq1 2768	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → (𝑥 = (𝑎 +o 𝑏) ↔ 𝑧 = (𝑎 +o 𝑏)))
83	82	2rexbidv 3229	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏)))
84		oveq1 7405	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑤 → (𝑎 +o 𝑏) = (𝑤 +o 𝑏))
85	84	eqeq2d 2775	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑤 → (𝑧 = (𝑎 +o 𝑏) ↔ 𝑧 = (𝑤 +o 𝑏)))
86		oveq2 7406	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑦 → (𝑤 +o 𝑏) = (𝑤 +o 𝑦))
87	86	eqeq2d 2775	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑦 → (𝑧 = (𝑤 +o 𝑏) ↔ 𝑧 = (𝑤 +o 𝑦)))
88	85, 87	cbvrex2vw 3247	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏) ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
89	83, 88	bitrdi 289	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦)))
90	81, 89	elab 3640	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
91	80, 90	sylibr 236	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
92	91	ralrimiva 3156	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ∀𝑧 ∈ (𝑎 +o 𝑏)𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
93	92	adantr 484	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → ∀𝑧 ∈ (𝑎 +o 𝑏)𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
94		simpr 488	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → 𝑦 = (𝑎 +o 𝑏))
95	93, 94	raleqtrrdv 3326	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
96	95	exp31 423	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
97	96	expdimp 456	. . . . . . . 8 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴) → (𝑏 ∈ 𝐵 → (𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
98	6, 12, 97	rexlimd 3271	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
99	98	ex 416	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑎 ∈ 𝐴 → (∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
100	1, 5, 99	rexlimd 3271	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
101	100	alrimiv 1949	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑦(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
102		eqeq1 2768	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 = (𝑎 +o 𝑏) ↔ 𝑦 = (𝑎 +o 𝑏)))
103	102	2rexbidv 3229	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏)))
104	103	ralab 3658	. . . 4 ⊢ (∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∀𝑦(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
105	101, 104	sylibr 236	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
106		dftr5 5213	. . 3 ⊢ (Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
107	105, 106	sylibr 236	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
108		simpr 488	. . . . . . 7 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → 𝑥 = (𝑎 +o 𝑏))
109	30	adantr 484	. . . . . . 7 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → (𝑎 +o 𝑏) ∈ On)
110	108, 109	eqeltrd 2864	. . . . . 6 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → 𝑥 ∈ On)
111	110	exp31 423	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑥 = (𝑎 +o 𝑏) → 𝑥 ∈ On)))
112	111	rexlimdvv 3220	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) → 𝑥 ∈ On))
113	112	abssdv 4022	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ On)
114		epweon 7760	. . 3 ⊢ E We On
115		wess 5635	. . 3 ⊢ ({𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ On → ( E We On → E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
116	113, 114, 115	mpisyl 21	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
117		df-ord 6351	. 2 ⊢ (Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ (Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ∧ E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
118	107, 116, 117	sylanbrc 592	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 858  ∀wal 1560   = wceq 1562   ∈ wcel 2144  {cab 2742   ≠ wne 2959  ∀wral 3078  ∃wrex 3088   ⊆ wss 3906   ⊊ wpss 3907  ∅c0 4287  Tr wtr 5209   E cep 5548   We wwe 5601  Ord word 6347  Oncon0 6348  (class class class)co 7398   +_o coa 8436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-rep 5229  ax-sep 5248  ax-nul 5258  ax-pr 5392  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3079  df-rex 3089  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-ov 7401  df-oprab 7402  df-mpo 7403  df-om 7849  df-2nd 7973  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-oadd 8443

This theorem is referenced by:  oaun3lem3  43958