Theorem maxssj0 36006

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 36004	. . . . 5 ⊢ 𝐽0 Isom 𝑅0, E ((On × On), On)
2		isof1o 7354	. . . . 5 ⊢ (𝐽0 Isom 𝑅0, E ((On × On), On) → 𝐽0:(On × On)⟶1-1ontoOn)
3		f1of 6846	. . . . 5 ⊢ (𝐽0:(On × On)⟶1-1ontoOn → 𝐽0:(On × On)⟶On)
4	1, 2, 3	mp2b 10	. . . 4 ⊢ 𝐽0:(On × On)⟶On
5		0elon 6436	. . . 4 ⊢ ∅ ∈ On
6	4, 5	f0cli 7122	. . 3 ⊢ (𝐽0‘⟨𝐴, 𝐵⟩) ∈ On
7	5	a1i 11	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∅ ∈ On)
8		onun2 6491	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ∈ On)
9	7, 8	opelxpd 5694	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ⟨∅, (𝐴 ∪ 𝐵)⟩ ∈ (On × On))
10		opelxpi 5692	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ⟨𝐴, 𝐵⟩ ∈ (On × On))
11		isorel 7357	. . . . . . 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 6921	. . . . . 6 ⊢ (𝐽0‘⟨𝐴, 𝐵⟩) ∈ V
15	14	epeli 5557	. . . . 5 ⊢ ((𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) E (𝐽0‘⟨𝐴, 𝐵⟩) ↔ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) ∈ (𝐽0‘⟨𝐴, 𝐵⟩))
16	13, 15	bitrdi 290	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) ∈ (𝐽0‘⟨𝐴, 𝐵⟩)))
17		fvex 6921	. . . . . . . . 9 ⊢ (𝐽0‘⟨∅, 𝑥⟩) ∈ V
18		eqid 2763	. . . . . . . . 9 ⊢ (𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩)) = (𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩))
19	17, 18	fnmpti 6704	. . . . . . . 8 ⊢ (𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩)) Fn On
20	18	j00smo 36005	. . . . . . . 8 ⊢ Smo (𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩))
21		smogt 8403	. . . . . . . 8 ⊢ (((𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩)) Fn On ∧ Smo (𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩)) ∧ (𝐴 ∪ 𝐵) ∈ On) → (𝐴 ∪ 𝐵) ⊆ ((𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩))‘(𝐴 ∪ 𝐵)))
22	19, 20, 21	mp3an12 1481	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐵) ∈ On → (𝐴 ∪ 𝐵) ⊆ ((𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩))‘(𝐴 ∪ 𝐵)))
23		opeq2 4844	. . . . . . . . 9 ⊢ (𝑥 = (𝐴 ∪ 𝐵) → ⟨∅, 𝑥⟩ = ⟨∅, (𝐴 ∪ 𝐵)⟩)
24	23	fveq2d 6912	. . . . . . . 8 ⊢ (𝑥 = (𝐴 ∪ 𝐵) → (𝐽0‘⟨∅, 𝑥⟩) = (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩))
25		fvex 6921	. . . . . . . 8 ⊢ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) ∈ V
26	24, 18, 25	fvmpt 7016	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐵) ∈ On → ((𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩))‘(𝐴 ∪ 𝐵)) = (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩))
27	22, 26	sseqtrd 3949	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∈ On → (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩))
28	8, 27	syl 18	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩))
29		ontr2 6429	. . . . . 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 6423	. . 3 ⊢ ((𝐽0‘⟨𝐴, 𝐵⟩) ∈ On → ((𝐴 ∪ 𝐵) ∈ (𝐽0‘⟨𝐴, 𝐵⟩) → (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨𝐴, 𝐵⟩)))
34	6, 32, 33	mpsylsyld 70	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ → (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨𝐴, 𝐵⟩)))
35		eqcom 2770	. . . . . . 7 ⊢ (𝐴 = ∅ ↔ ∅ = 𝐴)
36	35	biimpi 219	. . . . . 6 ⊢ (𝐴 = ∅ → ∅ = 𝐴)
37		uneq1 4163	. . . . . . 7 ⊢ (𝐴 = ∅ → (𝐴 ∪ 𝐵) = (∅ ∪ 𝐵))
38		0un 4349	. . . . . . 7 ⊢ (∅ ∪ 𝐵) = 𝐵
39	37, 38	eqtrdi 2814	. . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∪ 𝐵) = 𝐵)
40	36, 39	opeq12d 4851	. . . . 5 ⊢ (𝐴 = ∅ → ⟨∅, (𝐴 ∪ 𝐵)⟩ = ⟨𝐴, 𝐵⟩)
41	40	fveq2d 6912	. . . 4 ⊢ (𝐴 = ∅ → (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) = (𝐽0‘⟨𝐴, 𝐵⟩))
42	41	sseq2d 3945	. . 3 ⊢ (𝐴 = ∅ → ((𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨∅, (𝐴 ∪ 𝐵)⟩) ↔ (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨𝐴, 𝐵⟩)))
43	28, 42	syl5ibcom 248	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 = ∅ → (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨𝐴, 𝐵⟩)))
44		0un 4349	. . . . . . 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 36001	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩𝑅0⟨𝐴, 𝐵⟩ ↔ ((∅ ∪ (𝐴 ∪ 𝐵)) ∈ (𝐴 ∪ 𝐵) ∨ ((∅ ∪ (𝐴 ∪ 𝐵)) = (𝐴 ∪ 𝐵) ∧ ⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩))))
49		eloni 6390	. . . . . . . . . 10 ⊢ ((𝐴 ∪ 𝐵) ∈ On → Ord (𝐴 ∪ 𝐵))
50		ordirr 6398	. . . . . . . . . 10 ⊢ (Ord (𝐴 ∪ 𝐵) → ¬ (𝐴 ∪ 𝐵) ∈ (𝐴 ∪ 𝐵))
51	8, 49, 50	3syl 19	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ¬ (𝐴 ∪ 𝐵) ∈ (𝐴 ∪ 𝐵))
52	44	eleq1i 2855	. . . . . . . . 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 35999	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨∅, (𝐴 ∪ 𝐵)⟩LexOrd⟨𝐴, 𝐵⟩ ↔ (∅ ∈ 𝐴 ∨ (∅ = 𝐴 ∧ (𝐴 ∪ 𝐵) ∈ 𝐵))))
61		eloni 6390	. . . . . . . . . . 11 ⊢ (𝐵 ∈ On → Ord 𝐵)
62		ordirr 6398	. . . . . . . . . . 11 ⊢ (Ord 𝐵 → ¬ 𝐵 ∈ 𝐵)
63	61, 62	syl 18	. . . . . . . . . 10 ⊢ (𝐵 ∈ On → ¬ 𝐵 ∈ 𝐵)
64	63	intnand 494	. . . . . . . . 9 ⊢ (𝐵 ∈ On → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐵))
65	64	adantl 487	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐵))
66		onunel 6488	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∪ 𝐵) ∈ 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐵)))
67	66	3anidm23 1449	. . . . . . . 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 6438	. . . . . 6 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
76	75	adantr 486	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
77		df-ne 2960	. . . . 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 1570   ∈ wcel 2147   ≠ wne 2959   ⊆ wss 3900   ∪ cun 4152  ∅c0 4281  ⟨cop 4838   class class class wbr 5106   ↦ cmpt 5189   E cep 5554   × cxp 5653  Ord word 6379  Oncon0 6380   Fn wfn 6553  ⟶wf 6554  ⟶1-1ontowf1o 6557  ‘cfv 6558   Isom wiso 6559  Smo wsmo 8381  LexOrdclexo 35980  𝑅₀cr0 35981  𝐽₀ccj0 35982

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-isom 6567  df-riota 7400  df-ov 7446  df-1st 8025  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-smo 8382  df-recs 8407  df-oi 9531  df-lexo 35989  df-r0 35990  df-j0 35991

This theorem is used by:  k1le  36021  k2le  36022  k3n0k1lt  36023  k3n0k2lt  36024