Metamath Proof Explorer

Theorem nosepdmlem

Description: Lemma for nosepdm . (Contributed by Scott Fenton, 24-Nov-2021)

Ref Expression
Assertion nosepdmlem ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ ( dom 𝐴 ∪ dom 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sltval2 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ) )
2 fvex ⊢ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ∈ V
3 fvex ⊢ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ∈ V
4 2 3 brtp ⊢ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ↔ ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
5 df-3or ⊢ ( ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) ↔ ( ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
6 ndmfv ⊢ ( ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ )
7 1oex ⊢ 1o ∈ V
8 7 prid1 ⊢ 1o ∈ { 1o , 2o }
9 8 nosgnn0i ⊢ ∅ ≠ 1o
10 neeq1 ⊢ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ → ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ 1o ↔ ∅ ≠ 1o ) )
11 9 10 mpbiri ⊢ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ 1o )
12 11 neneqd ⊢ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ → ¬ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o )
13 12 intnanrd ⊢ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ → ¬ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) )
14 12 intnanrd ⊢ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ → ¬ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) )
15 ioran ⊢ ( ¬ ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) ↔ ( ¬ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∧ ¬ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
16 13 14 15 sylanbrc ⊢ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ → ¬ ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
17 6 16 syl ⊢ ( ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 → ¬ ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
18 17 adantl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 ) → ¬ ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
19 orel1 ⊢ ( ¬ ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) → ( ( ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) → ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
20 18 19 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 ) → ( ( ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) → ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
21 5 20 biimtrid ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 ) → ( ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) → ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
22 ndmfv ⊢ ( ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 → ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ )
23 2on ⊢ 2o ∈ On
24 23 elexi ⊢ 2o ∈ V
25 24 prid2 ⊢ 2o ∈ { 1o , 2o }
26 25 nosgnn0i ⊢ ∅ ≠ 2o
27 neeq1 ⊢ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ → ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ 2o ↔ ∅ ≠ 2o ) )
28 26 27 mpbiri ⊢ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ → ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ 2o )
29 22 28 syl ⊢ ( ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 → ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ 2o )
30 29 neneqd ⊢ ( ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 → ¬ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o )
31 30 con4i ⊢ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 )
32 31 adantl ⊢ ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 )
33 21 32 syl6 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 ) → ( ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 ) )
34 33 ex ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 → ( ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 ) ) )
35 34 com23 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) → ( ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 ) ) )
36 4 35 biimtrid ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 ) ) )
37 1 36 sylbid ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 → ( ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 ) ) )
38 37 3impia ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵 ) → ( ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 ) )
39 38 orrd ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵 ) → ( ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 ∨ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 ) )
40 elun ⊢ ( ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ ( dom 𝐴 ∪ dom 𝐵 ) ↔ ( ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 ∨ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 ) )
41 39 40 sylibr ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ ( dom 𝐴 ∪ dom 𝐵 ) )