Theorem oaun3lem1 44319

Description: The class of all ordinal sums of elements from two ordinals is ordinal. Lemma for oaun3 44327. (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 1947	. . . . . 6 ⊢ Ⅎ𝑎(𝐴 ∈ On ∧ 𝐵 ∈ On)
2		nfcv 2922	. . . . . . 7 ⊢ Ⅎ𝑎𝑦
3		nfre1 3287	. . . . . . . 8 ⊢ Ⅎ𝑎∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
4	3	nfsab 2750	. . . . . . 7 ⊢ Ⅎ𝑎 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
5	2, 4	nfralw 3309	. . . . . 6 ⊢ Ⅎ𝑎∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
6		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑏((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴)
7		nfcv 2922	. . . . . . . . 9 ⊢ Ⅎ𝑏𝑦
8		nfcv 2922	. . . . . . . . . . 11 ⊢ Ⅎ𝑏𝐴
9		nfre1 3287	. . . . . . . . . . 11 ⊢ Ⅎ𝑏∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
10	8, 9	nfrexw 3310	. . . . . . . . . 10 ⊢ Ⅎ𝑏∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)
11	10	nfsab 2750	. . . . . . . . 9 ⊢ Ⅎ𝑏 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
12	7, 11	nfralw 3309	. . . . . . . 8 ⊢ Ⅎ𝑏∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}
13		simp-4l 795	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → 𝐴 ∈ On)
14		simplrl 789	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑎 ∈ 𝐴)
15	14	anim1ci 628	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → (𝑧 ∈ 𝑎 ∧ 𝑎 ∈ 𝐴))
16		ontr1 6399	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ On → ((𝑧 ∈ 𝑎 ∧ 𝑎 ∈ 𝐴) → 𝑧 ∈ 𝐴))
17	13, 15, 16	sylc 66	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → 𝑧 ∈ 𝐴)
18		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐵 ∈ On)
19		ne0i 4286	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ 𝐵 → 𝐵 ≠ ∅)
20	19	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐵 ≠ ∅)
21		on0eln0 6409	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅))
22	21	biimpar 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ On ∧ 𝐵 ≠ ∅) → ∅ ∈ 𝐵)
23	18, 20, 22	syl2an 608	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ∅ ∈ 𝐵)
24		onelon 6376	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ On ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ On)
25	24	ad2ant2r 760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ On)
26		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
27		onelon 6376	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 ∈ On ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ On)
28	18, 26, 27	syl2an 608	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ On)
29		oacl 8521	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +o 𝑏) ∈ On)
30	25, 28, 29	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ∈ On)
31		onelon 6376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 +o 𝑏) ∈ On ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ On)
32	30, 31	sylan 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ On)
33		oa0 8502	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ On → (𝑧 +o ∅) = 𝑧)
34	32, 33	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑧 +o ∅) = 𝑧)
35	34	eqcomd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 = (𝑧 +o ∅))
36		oveq2 7416	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → (𝑧 +o 𝑦) = (𝑧 +o ∅))
37	36	rspceeqv 3598	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ 𝐵 ∧ 𝑧 = (𝑧 +o ∅)) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
38	23, 35, 37	syl2an2r 698	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
39	38	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦))
40		oveq1 7415	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑧 → (𝑤 +o 𝑦) = (𝑧 +o 𝑦))
41	40	eqeq2d 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑧 → (𝑧 = (𝑤 +o 𝑦) ↔ 𝑧 = (𝑧 +o 𝑦)))
42	41	rexbidv 3186	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑧 → (∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦) ↔ ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦)))
43	42	rspcev 3576	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝑧 = (𝑧 +o 𝑦)) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
44	17, 39, 43	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑧 ∈ 𝑎) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
45	18	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝐵 ∈ On)
46	25, 45	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 ∈ On ∧ 𝐵 ∈ On))
47	46	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑎 ∈ On ∧ 𝐵 ∈ On))
48		oacl 8521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ On ∧ 𝐵 ∈ On) → (𝑎 +o 𝐵) ∈ On)
49	25, 45, 48	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝐵) ∈ On)
50		eloni 6361	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 +o 𝑏) ∈ On → Ord (𝑎 +o 𝑏))
51		eloni 6361	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 +o 𝐵) ∈ On → Ord (𝑎 +o 𝐵))
52	50, 51	anim12i 625	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 +o 𝑏) ∈ On ∧ (𝑎 +o 𝐵) ∈ On) → (Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)))
53	30, 49, 52	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)))
54	45, 25	jca 521	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝐵 ∈ On ∧ 𝑎 ∈ On))
55	26	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵)
56		oaordi 8532	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 ∈ On ∧ 𝑎 ∈ On) → (𝑏 ∈ 𝐵 → (𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵)))
57	54, 55, 56	sylc 66	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵))
58		ordelpss 6379	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)) → ((𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵) ↔ (𝑎 +o 𝑏) ⊊ (𝑎 +o 𝐵)))
59	58	biimpd 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord (𝑎 +o 𝑏) ∧ Ord (𝑎 +o 𝐵)) → ((𝑎 +o 𝑏) ∈ (𝑎 +o 𝐵) → (𝑎 +o 𝑏) ⊊ (𝑎 +o 𝐵)))
60	53, 57, 59	sylc 66	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ⊊ (𝑎 +o 𝐵))
61	60	pssssd 4047	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 +o 𝑏) ⊆ (𝑎 +o 𝐵))
62	61	sselda 3930	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ (𝑎 +o 𝐵))
63	62	anim1ci 628	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → (𝑎 ⊆ 𝑧 ∧ 𝑧 ∈ (𝑎 +o 𝐵)))
64		oawordex2 44271	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ⊆ 𝑧 ∧ 𝑧 ∈ (𝑎 +o 𝐵))) → ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧)
65	47, 63, 64	syl2an2r 698	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧)
66		oveq1 7415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑎 → (𝑤 +o 𝑦) = (𝑎 +o 𝑦))
67	66	eqeq2d 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑎 → (𝑧 = (𝑤 +o 𝑦) ↔ 𝑧 = (𝑎 +o 𝑦)))
68		eqcom 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑎 +o 𝑦) ↔ (𝑎 +o 𝑦) = 𝑧)
69	67, 68	bitrdi 290	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑎 → (𝑧 = (𝑤 +o 𝑦) ↔ (𝑎 +o 𝑦) = 𝑧))
70	69	rexbidv 3186	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑎 → (∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦) ↔ ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧))
71	70	rspcev 3576	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 (𝑎 +o 𝑦) = 𝑧) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
72	14, 65, 71	syl2an2r 698	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) ∧ 𝑎 ⊆ 𝑧) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
73		eloni 6361	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ On → Ord 𝑧)
74	32, 73	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → Ord 𝑧)
75		eloni 6361	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ On → Ord 𝑎)
76	25, 75	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → Ord 𝑎)
77	76	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → Ord 𝑎)
78		ordtri2or 6452	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝑧 ∧ Ord 𝑎) → (𝑧 ∈ 𝑎 ∨ 𝑎 ⊆ 𝑧))
79	74, 77, 78	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → (𝑧 ∈ 𝑎 ∨ 𝑎 ⊆ 𝑧))
80	44, 72, 79	mpjaodan 973	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
81		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
82		eqeq1 2764	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → (𝑥 = (𝑎 +o 𝑏) ↔ 𝑧 = (𝑎 +o 𝑏)))
83	82	2rexbidv 3227	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏)))
84		oveq1 7415	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑤 → (𝑎 +o 𝑏) = (𝑤 +o 𝑏))
85	84	eqeq2d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑤 → (𝑧 = (𝑎 +o 𝑏) ↔ 𝑧 = (𝑤 +o 𝑏)))
86		oveq2 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑦 → (𝑤 +o 𝑏) = (𝑤 +o 𝑦))
87	86	eqeq2d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑦 → (𝑧 = (𝑤 +o 𝑏) ↔ 𝑧 = (𝑤 +o 𝑦)))
88	85, 87	cbvrex2vw 3245	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏) ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
89	83, 88	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦)))
90	81, 89	elab 3632	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∃𝑤 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑤 +o 𝑦))
91	80, 90	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑧 ∈ (𝑎 +o 𝑏)) → 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
92	91	ralrimiva 3154	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ∀𝑧 ∈ (𝑎 +o 𝑏)𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
93	92	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → ∀𝑧 ∈ (𝑎 +o 𝑏)𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
94		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → 𝑦 = (𝑎 +o 𝑏))
95	93, 94	raleqtrrdv 3323	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑦 = (𝑎 +o 𝑏)) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
96	95	exp31 425	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
97	96	expdimp 458	. . . . . . . 8 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴) → (𝑏 ∈ 𝐵 → (𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
98	6, 12, 97	rexlimd 3269	. . . . . . 7 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑎 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
99	98	ex 418	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑎 ∈ 𝐴 → (∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})))
100	1, 5, 99	rexlimd 3269	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
101	100	alrimiv 1960	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑦(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
102		eqeq1 2764	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 = (𝑎 +o 𝑏) ↔ 𝑦 = (𝑎 +o 𝑏)))
103	102	2rexbidv 3227	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏)))
104	103	ralab 3650	. . . 4 ⊢ (∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∀𝑦(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑦 = (𝑎 +o 𝑏) → ∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
105	101, 104	sylibr 237	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
106		dftr5 5215	. . 3 ⊢ (Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ ∀𝑦 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}∀𝑧 ∈ 𝑦 𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
107	105, 106	sylibr 237	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
108		simpr 490	. . . . . . 7 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → 𝑥 = (𝑎 +o 𝑏))
109	30	adantr 486	. . . . . . 7 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → (𝑎 +o 𝑏) ∈ On)
110	108, 109	eqeltrd 2860	. . . . . 6 ⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎 +o 𝑏)) → 𝑥 ∈ On)
111	110	exp31 425	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑥 = (𝑎 +o 𝑏) → 𝑥 ∈ On)))
112	111	rexlimdvv 3218	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏) → 𝑥 ∈ On))
113	112	abssdv 4014	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ On)
114		epweon 7772	. . 3 ⊢ E We On
115		wess 5633	. . 3 ⊢ ({𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ On → ( E We On → E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
116	113, 114, 115	mpisyl 22	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
117		df-ord 6354	. 2 ⊢ (Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ↔ (Tr {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ∧ E We {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}))
118	107, 116, 117	sylanbrc 595	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861  ∀wal 1568   = wceq 1570   ∈ wcel 2145  {cab 2738   ≠ wne 2955  ∀wral 3076  ∃wrex 3086   ⊆ wss 3898   ⊊ wpss 3899  ∅c0 4278  Tr wtr 5211   E cep 5546   We wwe 5599  Ord word 6350  Oncon0 6351  (class class class)co 7408   +_o coa 8451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6293  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7861  df-2nd 7985  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-oadd 8458

This theorem is used by:  oaun3lem3  44321