Metamath Proof Explorer

Theorem maxssj0

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

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

Proof

Step Hyp Ref Expression
1 j0iso ⊢ 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On )
2 isof1o ⊢ ( 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On ) → 𝐽0 : ( On × On ) –1-1-onto→ On )
3 f1of ⊢ ( 𝐽0 : ( On × On ) –1-1-onto→ On → 𝐽0 : ( On × On ) ⟶ On )
4 1 2 3 mp2b ⊢ 𝐽0 : ( On × On ) ⟶ On
5 0elon ⊢ ∅ ∈ On
6 4 5 f0cli ⊢ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On
7 5 a1i ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∅ ∈ On )
8 onun2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ 𝐵 ) ∈ On )
9 7 8 opelxpd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ∈ ( On × On ) )
10 opelxpi ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( On × On ) )
11 isorel ⊢ ( ( 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On ) ∧ ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ∈ ( On × On ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( On × On ) ) ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) E ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
12 1 11 mpan ⊢ ( ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ∈ ( On × On ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( On × On ) ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) E ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
13 9 10 12 syl2anc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) E ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
14 fvex ⊢ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V
15 14 epeli ⊢ ( ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) E ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) ∈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
16 13 15 bitrdi ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) ∈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
17 fvex ⊢ ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) ∈ V
18 eqid ⊢ ( 𝑥 ∈ On ↦ ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) ) = ( 𝑥 ∈ On ↦ ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) )
19 17 18 fnmpti ⊢ ( 𝑥 ∈ On ↦ ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) ) Fn On
20 18 j00smo ⊢ Smo ( 𝑥 ∈ On ↦ ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) )
21 smogt ⊢ ( ( ( 𝑥 ∈ On ↦ ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) ) Fn On ∧ Smo ( 𝑥 ∈ On ↦ ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) ) ∧ ( 𝐴 ∪ 𝐵 ) ∈ On ) → ( 𝐴 ∪ 𝐵 ) ⊆ ( ( 𝑥 ∈ On ↦ ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) ) ‘ ( 𝐴 ∪ 𝐵 ) ) )
22 19 20 21 mp3an12 ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ On → ( 𝐴 ∪ 𝐵 ) ⊆ ( ( 𝑥 ∈ On ↦ ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) ) ‘ ( 𝐴 ∪ 𝐵 ) ) )
23 opeq2 ⊢ ( 𝑥 = ( 𝐴 ∪ 𝐵 ) → ⟨ ∅ , 𝑥 ⟩ = ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ )
24 23 fveq2d ⊢ ( 𝑥 = ( 𝐴 ∪ 𝐵 ) → ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) = ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) )
25 fvex ⊢ ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) ∈ V
26 24 18 25 fvmpt ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ On → ( ( 𝑥 ∈ On ↦ ( 𝐽0 ‘ ⟨ ∅ , 𝑥 ⟩ ) ) ‘ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) )
27 22 26 sseqtrd ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ On → ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) )
28 8 27 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) )
29 ontr2 ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∈ On ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On ) → ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) ∧ ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) ∈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
30 8 6 29 sylancl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) ∧ ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) ∈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
31 28 30 mpand ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) ∈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
32 16 31 sylbid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ → ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
33 onelss ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On → ( ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
34 6 32 33 mpsylsyld ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ → ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
35 eqcom ⊢ ( 𝐴 = ∅ ↔ ∅ = 𝐴 )
36 35 biimpi ⊢ ( 𝐴 = ∅ → ∅ = 𝐴 )
37 uneq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ∪ 𝐵 ) = ( ∅ ∪ 𝐵 ) )
38 0un ⊢ ( ∅ ∪ 𝐵 ) = 𝐵
39 37 38 eqtrdi ⊢ ( 𝐴 = ∅ → ( 𝐴 ∪ 𝐵 ) = 𝐵 )
40 36 39 opeq12d ⊢ ( 𝐴 = ∅ → ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
41 40 fveq2d ⊢ ( 𝐴 = ∅ → ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) = ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
42 41 sseq2d ⊢ ( 𝐴 = ∅ → ( ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐽0 ‘ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
43 28 42 syl5ibcom ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 = ∅ → ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
44 0un ⊢ ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐴 ∪ 𝐵 )
45 44 a1i ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐴 ∪ 𝐵 ) )
46 simpl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ∈ On )
47 simpr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐵 ∈ On )
48 7 8 46 47 brr0d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ↔ ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ ( 𝐴 ∪ 𝐵 ) ∨ ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐴 ∪ 𝐵 ) ∧ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ LexOrd ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
49 eloni ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ On → Ord ( 𝐴 ∪ 𝐵 ) )
50 ordirr ⊢ ( Ord ( 𝐴 ∪ 𝐵 ) → ¬ ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐴 ∪ 𝐵 ) )
51 8 49 50 3syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ¬ ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐴 ∪ 𝐵 ) )
52 44 eleq1i ⊢ ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐴 ∪ 𝐵 ) )
53 51 52 sylnibr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ¬ ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ ( 𝐴 ∪ 𝐵 ) )
54 orel1 ⊢ ( ¬ ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ ( 𝐴 ∪ 𝐵 ) → ( ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ ( 𝐴 ∪ 𝐵 ) ∨ ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐴 ∪ 𝐵 ) ∧ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ LexOrd ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐴 ∪ 𝐵 ) ∧ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ LexOrd ⟨ 𝐴 , 𝐵 ⟩ ) ) )
55 olc ⊢ ( ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐴 ∪ 𝐵 ) ∧ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ LexOrd ⟨ 𝐴 , 𝐵 ⟩ ) → ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ ( 𝐴 ∪ 𝐵 ) ∨ ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐴 ∪ 𝐵 ) ∧ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ LexOrd ⟨ 𝐴 , 𝐵 ⟩ ) ) )
56 54 55 impbid1 ⊢ ( ¬ ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ ( 𝐴 ∪ 𝐵 ) → ( ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ ( 𝐴 ∪ 𝐵 ) ∨ ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐴 ∪ 𝐵 ) ∧ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ LexOrd ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐴 ∪ 𝐵 ) ∧ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ LexOrd ⟨ 𝐴 , 𝐵 ⟩ ) ) )
57 53 56 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ ( 𝐴 ∪ 𝐵 ) ∨ ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐴 ∪ 𝐵 ) ∧ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ LexOrd ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐴 ∪ 𝐵 ) ∧ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ LexOrd ⟨ 𝐴 , 𝐵 ⟩ ) ) )
58 48 57 bitrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ↔ ( ( ∅ ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐴 ∪ 𝐵 ) ∧ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ LexOrd ⟨ 𝐴 , 𝐵 ⟩ ) ) )
59 45 58 mpbirand ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ LexOrd ⟨ 𝐴 , 𝐵 ⟩ ) )
60 7 8 46 47 brlexod ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ LexOrd ⟨ 𝐴 , 𝐵 ⟩ ↔ ( ∅ ∈ 𝐴 ∨ ( ∅ = 𝐴 ∧ ( 𝐴 ∪ 𝐵 ) ∈ 𝐵 ) ) ) )
61 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
62 ordirr ⊢ ( Ord 𝐵 → ¬ 𝐵 ∈ 𝐵 )
63 61 62 syl ⊢ ( 𝐵 ∈ On → ¬ 𝐵 ∈ 𝐵 )
64 63 intnand ⊢ ( 𝐵 ∈ On → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐵 ) )
65 64 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐵 ) )
66 onunel ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ∪ 𝐵 ) ∈ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐵 ) ) )
67 66 3anidm23 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ∪ 𝐵 ) ∈ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐵 ) ) )
68 65 67 mtbird ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ¬ ( 𝐴 ∪ 𝐵 ) ∈ 𝐵 )
69 68 intnand ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ¬ ( ∅ = 𝐴 ∧ ( 𝐴 ∪ 𝐵 ) ∈ 𝐵 ) )
70 orel2 ⊢ ( ¬ ( ∅ = 𝐴 ∧ ( 𝐴 ∪ 𝐵 ) ∈ 𝐵 ) → ( ( ∅ ∈ 𝐴 ∨ ( ∅ = 𝐴 ∧ ( 𝐴 ∪ 𝐵 ) ∈ 𝐵 ) ) → ∅ ∈ 𝐴 ) )
71 orc ⊢ ( ∅ ∈ 𝐴 → ( ∅ ∈ 𝐴 ∨ ( ∅ = 𝐴 ∧ ( 𝐴 ∪ 𝐵 ) ∈ 𝐵 ) ) )
72 70 71 impbid1 ⊢ ( ¬ ( ∅ = 𝐴 ∧ ( 𝐴 ∪ 𝐵 ) ∈ 𝐵 ) → ( ( ∅ ∈ 𝐴 ∨ ( ∅ = 𝐴 ∧ ( 𝐴 ∪ 𝐵 ) ∈ 𝐵 ) ) ↔ ∅ ∈ 𝐴 ) )
73 69 72 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ∅ ∈ 𝐴 ∨ ( ∅ = 𝐴 ∧ ( 𝐴 ∪ 𝐵 ) ∈ 𝐵 ) ) ↔ ∅ ∈ 𝐴 ) )
74 59 60 73 3bitrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ↔ ∅ ∈ 𝐴 ) )
75 on0eln0 ⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
76 75 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
77 df-ne ⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
78 76 77 bitrdi ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐴 ↔ ¬ 𝐴 = ∅ ) )
79 74 78 bitrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ↔ ¬ 𝐴 = ∅ ) )
80 xor3 ⊢ ( ¬ ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝐴 = ∅ ) ↔ ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ↔ ¬ 𝐴 = ∅ ) )
81 nbior ⊢ ( ¬ ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝐴 = ∅ ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ∨ 𝐴 = ∅ ) )
82 80 81 sylbir ⊢ ( ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ↔ ¬ 𝐴 = ∅ ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ∨ 𝐴 = ∅ ) )
83 79 82 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ⟨ ∅ , ( 𝐴 ∪ 𝐵 ) ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ∨ 𝐴 = ∅ ) )
84 34 43 83 mpjaod ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )