Theorem maxssj0 35938

Description: The value of 𝐽₀ is at least the maximum of its two arguments. Proposition 15.1(1) of [TakeutiZaring] p. 154. (Contributed by BTernaryTau, 22-Sep-2026.)

Assertion

Ref	Expression
maxssj0	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨𝐴, 𝐵⟩))

Proof of Theorem maxssj0

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		j0iso 35936	. . . . 5 ⊢ 𝐽0 Isom 𝑅0, E ((On × On), On)
2		isof1o 7331	. . . . 5 ⊢ (𝐽0 Isom 𝑅0, E ((On × On), On) → 𝐽0:(On × On)–1-1-onto→On)
3		f1of 6824	. . . . 5 ⊢ (𝐽0:(On × On)–1-1-onto→On → 𝐽0:(On × On)⟶On)
4	1, 2, 3	mp2b 10	. . . 4 ⊢ 𝐽0:(On × On)⟶On
5		0elon 6418	. . . 4 ⊢ ∅ ∈ On
6	4, 5	f0cli 7098	. . 3 ⊢ (𝐽0‘⟨𝐴, 𝐵⟩) ∈ On
7	5	a1i 11	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∅ ∈ On)
8		onun2 6473	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ∈ On)
9	7, 8	opelxpd 5689	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ⟨∅, (𝐴 ∪ 𝐵)⟩ ∈ (On × On))
10		opelxpi 5687	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ⟨𝐴, 𝐵⟩ ∈ (On × On))
11		isorel 7334	. . . . . . 7 ⊢ ((𝐽0 Isom 𝑅0, E ((On × On), On) ∧ (⟨∅, (𝐴 ∪ 𝐵)⟩ ∈ (On × On) ∧ ⟨𝐴, 𝐵⟩ ∈ (On × On))) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) E (𝐽0‘⟨𝐴, 𝐵⟩)))
12	1, 11	mpan 703	. . . . . 6 ⊢ ((⟨∅, (𝐴 ∪ 𝐵)⟩ ∈ (On × On) ∧ ⟨𝐴, 𝐵⟩ ∈ (On × On)) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) E (𝐽0‘⟨𝐴, 𝐵⟩)))
13	9, 10, 12	syl2anc 596	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) E (𝐽0‘⟨𝐴, 𝐵⟩)))
14		fvex 6898	. . . . . 6 ⊢ (𝐽0‘⟨𝐴, 𝐵⟩) ∈ V
15	14	epeli 5552	. . . . 5 ⊢ ((𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) E (𝐽0‘⟨𝐴, 𝐵⟩) ↔ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) ∈ (𝐽0‘⟨𝐴, 𝐵⟩))
16	13, 15	bitrdi 290	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) ∈ (𝐽0‘⟨𝐴, 𝐵⟩)))
17		fvex 6898	. . . . . . . . 9 ⊢ (𝐽0‘⟨∅, 𝑥⟩) ∈ V
18		eqid 2760	. . . . . . . . 9 ⊢ (𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩)) = (𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩))
19	17, 18	fnmpti 6682	. . . . . . . 8 ⊢ (𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩)) Fn On
20	18	j00smo 35937	. . . . . . . 8 ⊢ Smo (𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩))
21		smogt 8376	. . . . . . . 8 ⊢ (((𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩)) Fn On ∧ Smo (𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩)) ∧ (𝐴 ∪ 𝐵) ∈ On) → (𝐴 ∪ 𝐵) ⊆ ((𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩))‘(𝐴 ∪ 𝐵)))
22	19, 20, 21	mp3an12 1480	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐵) ∈ On → (𝐴 ∪ 𝐵) ⊆ ((𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩))‘(𝐴 ∪ 𝐵)))
23		opeq2 4833	. . . . . . . . 9 ⊢ (𝑥 = (𝐴 ∪ 𝐵) → ⟨∅, 𝑥⟩ = ⟨∅, (𝐴 ∪ 𝐵)⟩)
24	23	fveq2d 6889	. . . . . . . 8 ⊢ (𝑥 = (𝐴 ∪ 𝐵) → (𝐽0‘⟨∅, 𝑥⟩) = (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩))
25		fvex 6898	. . . . . . . 8 ⊢ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) ∈ V
26	24, 18, 25	fvmpt 6993	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐵) ∈ On → ((𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩))‘(𝐴 ∪ 𝐵)) = (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩))
27	22, 26	sseqtrd 3944	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∈ On → (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩))
28	8, 27	syl 18	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩))
29		ontr2 6411	. . . . . 6 ⊢ (((𝐴 ∪ 𝐵) ∈ On ∧ (𝐽0‘⟨𝐴, 𝐵⟩) ∈ On) → (((𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) ∧ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) ∈ (𝐽0‘⟨𝐴, 𝐵⟩)) → (𝐴 ∪ 𝐵) ∈ (𝐽0‘⟨𝐴, 𝐵⟩)))
30	8, 6, 29	sylancl 598	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (((𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) ∧ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) ∈ (𝐽0‘⟨𝐴, 𝐵⟩)) → (𝐴 ∪ 𝐵) ∈ (𝐽0‘⟨𝐴, 𝐵⟩)))
31	28, 30	mpand 708	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) ∈ (𝐽0‘⟨𝐴, 𝐵⟩) → (𝐴 ∪ 𝐵) ∈ (𝐽0‘⟨𝐴, 𝐵⟩)))
32	16, 31	sylbid 243	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ → (𝐴 ∪ 𝐵) ∈ (𝐽0‘⟨𝐴, 𝐵⟩)))
33		onelss 6405	. . 3 ⊢ ((𝐽0‘⟨𝐴, 𝐵⟩) ∈ On → ((𝐴 ∪ 𝐵) ∈ (𝐽0‘⟨𝐴, 𝐵⟩) → (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨𝐴, 𝐵⟩)))
34	6, 32, 33	mpsylsyld 70	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ → (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨𝐴, 𝐵⟩)))
35		eqcom 2767	. . . . . . 7 ⊢ (𝐴 = ∅ ↔ ∅ = 𝐴)
36	35	biimpi 219	. . . . . 6 ⊢ (𝐴 = ∅ → ∅ = 𝐴)
37		uneq1 4160	. . . . . . 7 ⊢ (𝐴 = ∅ → (𝐴 ∪ 𝐵) = (∅ ∪ 𝐵))
38		0un 4345	. . . . . . 7 ⊢ (∅ ∪ 𝐵) = 𝐵
39	37, 38	eqtrdi 2811	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∪ 𝐵) = 𝐵)
40	36, 39	opeq12d 4840	. . . . 5 ⊢ (𝐴 = ∅ → ⟨∅, (𝐴 ∪ 𝐵)⟩ = ⟨𝐴, 𝐵⟩)
41	40	fveq2d 6889	. . . 4 ⊢ (𝐴 = ∅ → (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) = (𝐽0‘⟨𝐴, 𝐵⟩))
42	41	sseq2d 3940	. . 3 ⊢ (𝐴 = ∅ → ((𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) ↔ (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨𝐴, 𝐵⟩)))
43	28, 42	syl5ibcom 248	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 = ∅ → (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨𝐴, 𝐵⟩)))
44		0un 4345	. . . . . . 7 ⊢ (∅ ∪ (𝐴 ∪ 𝐵)) = (𝐴 ∪ 𝐵)
45	44	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅ ∪ (𝐴 ∪ 𝐵)) = (𝐴 ∪ 𝐵))
46		simpl 488	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ∈ On)
47		simpr 490	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐵 ∈ On)
48	7, 8, 46, 47	brr0d 35933	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ ((∅ ∪ (𝐴 ∪ 𝐵)) ∈ (𝐴 ∪ 𝐵) ∨ ((∅ ∪ (𝐴 ∪ 𝐵)) = (𝐴 ∪ 𝐵) ∧ ⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩))))
49		eloni 6372	. . . . . . . . . 10 ⊢ ((𝐴 ∪ 𝐵) ∈ On → Ord (𝐴 ∪ 𝐵))
50		ordirr 6380	. . . . . . . . . 10 ⊢ (Ord (𝐴 ∪ 𝐵) → ¬ (𝐴 ∪ 𝐵) ∈ (𝐴 ∪ 𝐵))
51	8, 49, 50	3syl 19	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ¬ (𝐴 ∪ 𝐵) ∈ (𝐴 ∪ 𝐵))
52	44	eleq1i 2851	. . . . . . . . 9 ⊢ ((∅ ∪ (𝐴 ∪ 𝐵)) ∈ (𝐴 ∪ 𝐵) ↔ (𝐴 ∪ 𝐵) ∈ (𝐴 ∪ 𝐵))
53	51, 52	sylnibr 332	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ¬ (∅ ∪ (𝐴 ∪ 𝐵)) ∈ (𝐴 ∪ 𝐵))
54		orel1 902	. . . . . . . . 9 ⊢ (¬ (∅ ∪ (𝐴 ∪ 𝐵)) ∈ (𝐴 ∪ 𝐵) → (((∅ ∪ (𝐴 ∪ 𝐵)) ∈ (𝐴 ∪ 𝐵) ∨ ((∅ ∪ (𝐴 ∪ 𝐵)) = (𝐴 ∪ 𝐵) ∧ ⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩)) → ((∅ ∪ (𝐴 ∪ 𝐵)) = (𝐴 ∪ 𝐵) ∧ ⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩)))
55		olc 882	. . . . . . . . 9 ⊢ (((∅ ∪ (𝐴 ∪ 𝐵)) = (𝐴 ∪ 𝐵) ∧ ⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩) → ((∅ ∪ (𝐴 ∪ 𝐵)) ∈ (𝐴 ∪ 𝐵) ∨ ((∅ ∪ (𝐴 ∪ 𝐵)) = (𝐴 ∪ 𝐵) ∧ ⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩)))
56	54, 55	impbid1 228	. . . . . . . 8 ⊢ (¬ (∅ ∪ (𝐴 ∪ 𝐵)) ∈ (𝐴 ∪ 𝐵) → (((∅ ∪ (𝐴 ∪ 𝐵)) ∈ (𝐴 ∪ 𝐵) ∨ ((∅ ∪ (𝐴 ∪ 𝐵)) = (𝐴 ∪ 𝐵) ∧ ⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩)) ↔ ((∅ ∪ (𝐴 ∪ 𝐵)) = (𝐴 ∪ 𝐵) ∧ ⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩)))
57	53, 56	syl 18	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (((∅ ∪ (𝐴 ∪ 𝐵)) ∈ (𝐴 ∪ 𝐵) ∨ ((∅ ∪ (𝐴 ∪ 𝐵)) = (𝐴 ∪ 𝐵) ∧ ⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩)) ↔ ((∅ ∪ (𝐴 ∪ 𝐵)) = (𝐴 ∪ 𝐵) ∧ ⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩)))
58	48, 57	bitrd 282	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ ((∅ ∪ (𝐴 ∪ 𝐵)) = (𝐴 ∪ 𝐵) ∧ ⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩)))
59	45, 58	mpbirand 720	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ ⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩))
60	7, 8, 46, 47	brlexod 35931	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩ ↔ (∅ ∈ 𝐴 ∨ (∅ = 𝐴 ∧ (𝐴 ∪ 𝐵) ∈ 𝐵))))
61		eloni 6372	. . . . . . . . . . 11 ⊢ (𝐵 ∈ On → Ord 𝐵)
62		ordirr 6380	. . . . . . . . . . 11 ⊢ (Ord 𝐵 → ¬ 𝐵 ∈ 𝐵)
63	61, 62	syl 18	. . . . . . . . . 10 ⊢ (𝐵 ∈ On → ¬ 𝐵 ∈ 𝐵)
64	63	intnand 494	. . . . . . . . 9 ⊢ (𝐵 ∈ On → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐵))
65	64	adantl 487	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐵))
66		onunel 6470	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∪ 𝐵) ∈ 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐵)))
67	66	3anidm23 1448	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∪ 𝐵) ∈ 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐵)))
68	65, 67	mtbird 328	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ¬ (𝐴 ∪ 𝐵) ∈ 𝐵)
69	68	intnand 494	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ¬ (∅ = 𝐴 ∧ (𝐴 ∪ 𝐵) ∈ 𝐵))
70		orel2 904	. . . . . . 7 ⊢ (¬ (∅ = 𝐴 ∧ (𝐴 ∪ 𝐵) ∈ 𝐵) → ((∅ ∈ 𝐴 ∨ (∅ = 𝐴 ∧ (𝐴 ∪ 𝐵) ∈ 𝐵)) → ∅ ∈ 𝐴))
71		orc 881	. . . . . . 7 ⊢ (∅ ∈ 𝐴 → (∅ ∈ 𝐴 ∨ (∅ = 𝐴 ∧ (𝐴 ∪ 𝐵) ∈ 𝐵)))
72	70, 71	impbid1 228	. . . . . 6 ⊢ (¬ (∅ = 𝐴 ∧ (𝐴 ∪ 𝐵) ∈ 𝐵) → ((∅ ∈ 𝐴 ∨ (∅ = 𝐴 ∧ (𝐴 ∪ 𝐵) ∈ 𝐵)) ↔ ∅ ∈ 𝐴))
73	69, 72	syl 18	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((∅ ∈ 𝐴 ∨ (∅ = 𝐴 ∧ (𝐴 ∪ 𝐵) ∈ 𝐵)) ↔ ∅ ∈ 𝐴))
74	59, 60, 73	3bitrd 308	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ ∅ ∈ 𝐴))
75		on0eln0 6420	. . . . . 6 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
76	75	adantr 486	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
77		df-ne 2956	. . . . 5 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
78	76, 77	bitrdi 290	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅ ∈ 𝐴 ↔ ¬ 𝐴 = ∅))
79	74, 78	bitrd 282	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ ¬ 𝐴 = ∅))
80		xor3 385	. . . 4 ⊢ (¬ (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ 𝐴 = ∅) ↔ (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ ¬ 𝐴 = ∅))
81		nbior 901	. . . 4 ⊢ (¬ (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ 𝐴 = ∅) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ∨ 𝐴 = ∅))
82	80, 81	sylbir 238	. . 3 ⊢ ((⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ ¬ 𝐴 = ∅) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ∨ 𝐴 = ∅))
83	79, 82	syl 18	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ∨ 𝐴 = ∅))
84	34, 43, 83	mpjaod 874	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨𝐴, 𝐵⟩))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1569   ∈ wcel 2144   ≠ wne 2955   ⊆ wss 3895   ∪ cun 4149  ∅c0 4278  ⟨cop 4589   class class class wbr 5102   ↦ cmpt 5185   E cep 5549   × cxp 5648  Ord word 6361  Oncon0 6362   Fn wfn 6533  ⟶wf 6534  –1-1-onto→wf1o 6537  ‘cfv 6538   Isom wiso 6539  Smo wsmo 8354  LexOrdclexo 35912  𝑅₀cr0 35913  𝐽₀ccj0 35914

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  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 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-1st 8001  df-2nd 8002  df-frecs 8300  df-wrecs 8331  df-smo 8355  df-recs 8380  df-oi 9505  df-lexo 35921  df-r0 35922  df-j0 35923

This theorem is used by: (None)