Metamath Proof Explorer

Theorem noetasuplem4

Description: Lemma for noeta . When A and B are separated, then Z is a lower bound for B . Part of Theorem 5.1 of Lipparini p. 7-8. (Contributed by Scott Fenton, 7-Dec-2021)

Ref Expression
Hypotheses noetasuplem.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
noetasuplem.2 ⊢ 𝑍 = ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) )
Assertion noetasuplem4 ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 )

Proof

Step Hyp Ref Expression
1 noetasuplem.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 noetasuplem.2 ⊢ 𝑍 = ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) )
3 ralcom ⊢ ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ∀ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑏 )
4 simplll ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐴 ⊆ No )
5 simpllr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐴 ∈ V )
6 simprl ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) → 𝐵 ⊆ No )
7 6 sselda ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ No )
8 1 nosupbnd2 ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑏 ∈ No ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑏 ↔ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) )
9 4 5 7 8 syl3anc ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑏 ↔ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) )
10 simpl ⊢ ( ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) → 𝑏 ∈ 𝐵 )
11 ssel2 ⊢ ( ( 𝐵 ⊆ No ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ No )
12 6 10 11 syl2an ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → 𝑏 ∈ No )
13 nodmord ⊢ ( 𝑏 ∈ No → Ord dom 𝑏 )
14 ordirr ⊢ ( Ord dom 𝑏 → ¬ dom 𝑏 ∈ dom 𝑏 )
15 12 13 14 3syl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → ¬ dom 𝑏 ∈ dom 𝑏 )
16 ssun2 ⊢ suc ∪ ( bday “ 𝐵 ) ⊆ ( dom 𝑆 ∪ suc ∪ ( bday “ 𝐵 ) )
17 bdayval ⊢ ( 𝑏 ∈ No → ( bday ‘ 𝑏 ) = dom 𝑏 )
18 12 17 syl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → ( bday ‘ 𝑏 ) = dom 𝑏 )
19 bdayfo ⊢ bday : No –onto→ On
20 fofn ⊢ ( bday : No –onto→ On → bday Fn No )
21 19 20 ax-mp ⊢ bday Fn No
22 fnfvima ⊢ ( ( bday Fn No ∧ 𝐵 ⊆ No ∧ 𝑏 ∈ 𝐵 ) → ( bday ‘ 𝑏 ) ∈ ( bday “ 𝐵 ) )
23 21 22 mp3an1 ⊢ ( ( 𝐵 ⊆ No ∧ 𝑏 ∈ 𝐵 ) → ( bday ‘ 𝑏 ) ∈ ( bday “ 𝐵 ) )
24 6 10 23 syl2an ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → ( bday ‘ 𝑏 ) ∈ ( bday “ 𝐵 ) )
25 18 24 eqeltrrd ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → dom 𝑏 ∈ ( bday “ 𝐵 ) )
26 elssuni ⊢ ( dom 𝑏 ∈ ( bday “ 𝐵 ) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵 ) )
27 25 26 syl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵 ) )
28 nodmon ⊢ ( 𝑏 ∈ No → dom 𝑏 ∈ On )
29 imassrn ⊢ ( bday “ 𝐵 ) ⊆ ran bday
30 forn ⊢ ( bday : No –onto→ On → ran bday = On )
31 19 30 ax-mp ⊢ ran bday = On
32 29 31 sseqtri ⊢ ( bday “ 𝐵 ) ⊆ On
33 ssorduni ⊢ ( ( bday “ 𝐵 ) ⊆ On → Ord ∪ ( bday “ 𝐵 ) )
34 32 33 ax-mp ⊢ Ord ∪ ( bday “ 𝐵 )
35 ordsssuc ⊢ ( ( dom 𝑏 ∈ On ∧ Ord ∪ ( bday “ 𝐵 ) ) → ( dom 𝑏 ⊆ ∪ ( bday “ 𝐵 ) ↔ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) ) )
36 34 35 mpan2 ⊢ ( dom 𝑏 ∈ On → ( dom 𝑏 ⊆ ∪ ( bday “ 𝐵 ) ↔ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) ) )
37 12 28 36 3syl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → ( dom 𝑏 ⊆ ∪ ( bday “ 𝐵 ) ↔ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) ) )
38 27 37 mpbid ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) )
39 16 38 sselid ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → dom 𝑏 ∈ ( dom 𝑆 ∪ suc ∪ ( bday “ 𝐵 ) ) )
40 eleq2 ⊢ ( ( dom 𝑆 ∪ suc ∪ ( bday “ 𝐵 ) ) = dom 𝑏 → ( dom 𝑏 ∈ ( dom 𝑆 ∪ suc ∪ ( bday “ 𝐵 ) ) ↔ dom 𝑏 ∈ dom 𝑏 ) )
41 39 40 syl5ibcom ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → ( ( dom 𝑆 ∪ suc ∪ ( bday “ 𝐵 ) ) = dom 𝑏 → dom 𝑏 ∈ dom 𝑏 ) )
42 15 41 mtod ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → ¬ ( dom 𝑆 ∪ suc ∪ ( bday “ 𝐵 ) ) = dom 𝑏 )
43 2 dmeqi ⊢ dom 𝑍 = dom ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) )
44 dmun ⊢ dom ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) = ( dom 𝑆 ∪ dom ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) )
45 43 44 eqtri ⊢ dom 𝑍 = ( dom 𝑆 ∪ dom ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) )
46 1oex ⊢ 1o ∈ V
47 46 snnz ⊢ { 1o } ≠ ∅
48 dmxp ⊢ ( { 1o } ≠ ∅ → dom ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) = ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) )
49 47 48 ax-mp ⊢ dom ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) = ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 )
50 49 uneq2i ⊢ ( dom 𝑆 ∪ dom ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) = ( dom 𝑆 ∪ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) )
51 undif2 ⊢ ( dom 𝑆 ∪ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ) = ( dom 𝑆 ∪ suc ∪ ( bday “ 𝐵 ) )
52 45 50 51 3eqtri ⊢ dom 𝑍 = ( dom 𝑆 ∪ suc ∪ ( bday “ 𝐵 ) )
53 dmeq ⊢ ( 𝑍 = 𝑏 → dom 𝑍 = dom 𝑏 )
54 52 53 eqtr3id ⊢ ( 𝑍 = 𝑏 → ( dom 𝑆 ∪ suc ∪ ( bday “ 𝐵 ) ) = dom 𝑏 )
55 42 54 nsyl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → ¬ 𝑍 = 𝑏 )
56 df-ne ⊢ ( 𝑍 ≠ 𝑏 ↔ ¬ 𝑍 = 𝑏 )
57 notnotr ⊢ ( ¬ ¬ dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 → dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 )
58 simpr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 )
59 58 fvresd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑍 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
60 2 reseq1i ⊢ ( 𝑍 ↾ dom 𝑆 ) = ( ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) ↾ dom 𝑆 )
61 resundir ⊢ ( ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) ↾ dom 𝑆 ) = ( ( 𝑆 ↾ dom 𝑆 ) ∪ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) )
62 df-res ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) = ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ∩ ( dom 𝑆 × V ) )
63 disjdifr ⊢ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ∩ dom 𝑆 ) = ∅
64 xpdisj1 ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ∩ dom 𝑆 ) = ∅ → ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ∩ ( dom 𝑆 × V ) ) = ∅ )
65 63 64 ax-mp ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ∩ ( dom 𝑆 × V ) ) = ∅
66 62 65 eqtri ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) = ∅
67 66 uneq2i ⊢ ( ( 𝑆 ↾ dom 𝑆 ) ∪ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) ) = ( ( 𝑆 ↾ dom 𝑆 ) ∪ ∅ )
68 un0 ⊢ ( ( 𝑆 ↾ dom 𝑆 ) ∪ ∅ ) = ( 𝑆 ↾ dom 𝑆 )
69 67 68 eqtri ⊢ ( ( 𝑆 ↾ dom 𝑆 ) ∪ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) ) = ( 𝑆 ↾ dom 𝑆 )
70 60 61 69 3eqtri ⊢ ( 𝑍 ↾ dom 𝑆 ) = ( 𝑆 ↾ dom 𝑆 )
71 simplll ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
72 1 nosupno ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No )
73 71 72 syl ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝑆 ∈ No )
74 73 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → 𝑆 ∈ No )
75 nofun ⊢ ( 𝑆 ∈ No → Fun 𝑆 )
76 74 75 syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → Fun 𝑆 )
77 funrel ⊢ ( Fun 𝑆 → Rel 𝑆 )
78 resdm ⊢ ( Rel 𝑆 → ( 𝑆 ↾ dom 𝑆 ) = 𝑆 )
79 76 77 78 3syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑆 ↾ dom 𝑆 ) = 𝑆 )
80 70 79 eqtrid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑍 ↾ dom 𝑆 ) = 𝑆 )
81 80 fveq1d ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑍 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
82 59 81 eqtr3d ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
83 simp-4l ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝐴 ⊆ No )
84 simp-4r ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝐴 ∈ V )
85 simplrr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → 𝐵 ∈ V )
86 85 adantr ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝐵 ∈ V )
87 1 2 noetasuplem1 ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝑍 ∈ No )
88 83 84 86 87 syl3anc ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝑍 ∈ No )
89 88 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → 𝑍 ∈ No )
90 12 adantr ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝑏 ∈ No )
91 90 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → 𝑏 ∈ No )
92 simplr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → 𝑍 ≠ 𝑏 )
93 nosepne ⊢ ( ( 𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏 ) → ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( 𝑏 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
94 89 91 92 93 syl3anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( 𝑏 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
95 82 94 eqnetrrd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( 𝑏 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
96 58 fvresd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( 𝑏 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
97 95 96 neeqtrrd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
98 fveq2 ⊢ ( 𝑞 = ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } → ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
99 fveq2 ⊢ ( 𝑞 = ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } → ( 𝑆 ‘ 𝑞 ) = ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
100 98 99 neeq12d ⊢ ( 𝑞 = ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } → ( ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) ≠ ( 𝑆 ‘ 𝑞 ) ↔ ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ) )
101 df-ne ⊢ ( ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) ≠ ( 𝑆 ‘ 𝑞 ) ↔ ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) )
102 necom ⊢ ( ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ↔ ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
103 100 101 102 3bitr3g ⊢ ( 𝑞 = ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } → ( ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ↔ ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ) )
104 103 rspcev ⊢ ( ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ∧ ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ) → ∃ 𝑞 ∈ dom 𝑆 ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) )
105 58 97 104 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ∃ 𝑞 ∈ dom 𝑆 ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) )
106 rexeq ⊢ ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 → ( ∃ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ↔ ∃ 𝑞 ∈ dom 𝑆 ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
107 105 106 syl5ibrcom ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 → ∃ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
108 rexnal ⊢ ( ∃ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ↔ ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) )
109 107 108 imbitrdi ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 → ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
110 57 109 syl5 ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ¬ ¬ dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 → ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
111 110 orrd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ¬ dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∨ ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
112 nofun ⊢ ( 𝑏 ∈ No → Fun 𝑏 )
113 funres ⊢ ( Fun 𝑏 → Fun ( 𝑏 ↾ dom 𝑆 ) )
114 91 112 113 3syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → Fun ( 𝑏 ↾ dom 𝑆 ) )
115 eqfunfv ⊢ ( ( Fun ( 𝑏 ↾ dom 𝑆 ) ∧ Fun 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ↔ ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∧ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) ) )
116 114 76 115 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ↔ ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∧ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) ) )
117 ianor ⊢ ( ¬ ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∧ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) ↔ ( ¬ dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∨ ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
118 117 con1bii ⊢ ( ¬ ( ¬ dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∨ ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) ↔ ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∧ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
119 116 118 bitr4di ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ↔ ¬ ( ¬ dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∨ ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) ) )
120 119 con2bid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( ¬ dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∨ ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) ↔ ¬ ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ) )
121 111 120 mpbid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ¬ ( 𝑏 ↾ dom 𝑆 ) = 𝑆 )
122 121 pm2.21d ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 → 𝑍 <s 𝑏 ) )
123 80 breq1d ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑍 ↾ dom 𝑆 ) <s ( 𝑏 ↾ dom 𝑆 ) ↔ 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) ) )
124 nodmon ⊢ ( 𝑆 ∈ No → dom 𝑆 ∈ On )
125 74 124 syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → dom 𝑆 ∈ On )
126 ltsres ⊢ ( ( 𝑍 ∈ No ∧ 𝑏 ∈ No ∧ dom 𝑆 ∈ On ) → ( ( 𝑍 ↾ dom 𝑆 ) <s ( 𝑏 ↾ dom 𝑆 ) → 𝑍 <s 𝑏 ) )
127 89 91 125 126 syl3anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑍 ↾ dom 𝑆 ) <s ( 𝑏 ↾ dom 𝑆 ) → 𝑍 <s 𝑏 ) )
128 123 127 sylbird ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) → 𝑍 <s 𝑏 ) )
129 simplrr ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 )
130 129 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 )
131 noreson ⊢ ( ( 𝑏 ∈ No ∧ dom 𝑆 ∈ On ) → ( 𝑏 ↾ dom 𝑆 ) ∈ No )
132 91 125 131 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑏 ↾ dom 𝑆 ) ∈ No )
133 ltsso ⊢ <s Or No
134 sotric ⊢ ( ( <s Or No ∧ ( ( 𝑏 ↾ dom 𝑆 ) ∈ No ∧ 𝑆 ∈ No ) ) → ( ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ↔ ¬ ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ∨ 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) ) ) )
135 133 134 mpan ⊢ ( ( ( 𝑏 ↾ dom 𝑆 ) ∈ No ∧ 𝑆 ∈ No ) → ( ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ↔ ¬ ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ∨ 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) ) ) )
136 132 74 135 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ↔ ¬ ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ∨ 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) ) ) )
137 136 con2bid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ∨ 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) ) ↔ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) )
138 130 137 mpbird ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ∨ 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) ) )
139 122 128 138 mpjaod ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → 𝑍 <s 𝑏 )
140 88 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑍 ∈ No )
141 90 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑏 ∈ No )
142 simplr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑍 ≠ 𝑏 )
143 2 fveq1i ⊢ ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } )
144 simp-4l ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
145 144 72 75 3syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → Fun 𝑆 )
146 funfn ⊢ ( Fun 𝑆 ↔ 𝑆 Fn dom 𝑆 )
147 145 146 sylib ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑆 Fn dom 𝑆 )
148 46 fconst ⊢ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) : ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ⟶ { 1o }
149 ffn ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) : ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ⟶ { 1o } → ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) Fn ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) )
150 148 149 ax-mp ⊢ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) Fn ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 )
151 150 a1i ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) Fn ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) )
152 disjdif ⊢ ( dom 𝑆 ∩ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ) = ∅
153 152 a1i ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( dom 𝑆 ∩ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ) = ∅ )
154 necom ⊢ ( ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) ↔ ( 𝑏 ‘ 𝑝 ) ≠ ( 𝑍 ‘ 𝑝 ) )
155 154 rabbii ⊢ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } = { 𝑝 ∈ On ∣ ( 𝑏 ‘ 𝑝 ) ≠ ( 𝑍 ‘ 𝑝 ) }
156 155 inteqi ⊢ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } = ∩ { 𝑝 ∈ On ∣ ( 𝑏 ‘ 𝑝 ) ≠ ( 𝑍 ‘ 𝑝 ) }
157 142 necomd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑏 ≠ 𝑍 )
158 nosepssdm ⊢ ( ( 𝑏 ∈ No ∧ 𝑍 ∈ No ∧ 𝑏 ≠ 𝑍 ) → ∩ { 𝑝 ∈ On ∣ ( 𝑏 ‘ 𝑝 ) ≠ ( 𝑍 ‘ 𝑝 ) } ⊆ dom 𝑏 )
159 141 140 157 158 syl3anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ∩ { 𝑝 ∈ On ∣ ( 𝑏 ‘ 𝑝 ) ≠ ( 𝑍 ‘ 𝑝 ) } ⊆ dom 𝑏 )
160 156 159 eqsstrid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ⊆ dom 𝑏 )
161 141 17 syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( bday ‘ 𝑏 ) = dom 𝑏 )
162 simplrl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → 𝐵 ⊆ No )
163 162 adantr ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝐵 ⊆ No )
164 163 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝐵 ⊆ No )
165 simplrl ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝑏 ∈ 𝐵 )
166 165 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑏 ∈ 𝐵 )
167 164 166 23 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( bday ‘ 𝑏 ) ∈ ( bday “ 𝐵 ) )
168 161 167 eqeltrrd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → dom 𝑏 ∈ ( bday “ 𝐵 ) )
169 168 26 syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵 ) )
170 141 28 36 3syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( dom 𝑏 ⊆ ∪ ( bday “ 𝐵 ) ↔ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) ) )
171 169 170 mpbid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) )
172 nosepon ⊢ ( ( 𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏 ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ On )
173 140 141 142 172 syl3anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ On )
174 eloni ⊢ ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ On → Ord ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } )
175 ordsuc ⊢ ( Ord ∪ ( bday “ 𝐵 ) ↔ Ord suc ∪ ( bday “ 𝐵 ) )
176 34 175 mpbi ⊢ Ord suc ∪ ( bday “ 𝐵 )
177 ordtr2 ⊢ ( ( Ord ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∧ Ord suc ∪ ( bday “ 𝐵 ) ) → ( ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ suc ∪ ( bday “ 𝐵 ) ) )
178 176 177 mpan2 ⊢ ( Ord ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } → ( ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ suc ∪ ( bday “ 𝐵 ) ) )
179 173 174 178 3syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ suc ∪ ( bday “ 𝐵 ) ) )
180 160 171 179 mp2and ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ suc ∪ ( bday “ 𝐵 ) )
181 simpr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } )
182 144 72 124 3syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → dom 𝑆 ∈ On )
183 ontri1 ⊢ ( ( dom 𝑆 ∈ On ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ On ) → ( dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ↔ ¬ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) )
184 182 173 183 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ↔ ¬ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) )
185 181 184 mpbid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ¬ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 )
186 180 185 eldifd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) )
187 fvun2 ⊢ ( ( 𝑆 Fn dom 𝑆 ∧ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) Fn ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ∧ ( ( dom 𝑆 ∩ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ) = ∅ ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ) ) → ( ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
188 147 151 153 186 187 syl112anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
189 143 188 eqtrid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
190 46 fvconst2 ⊢ ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) → ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = 1o )
191 186 190 syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = 1o )
192 189 191 eqtrd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = 1o )
193 nosep1o ⊢ ( ( ( 𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏 ) ∧ ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = 1o ) → 𝑍 <s 𝑏 )
194 140 141 142 192 193 syl31anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑍 <s 𝑏 )
195 simpr ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝑍 ≠ 𝑏 )
196 88 90 195 172 syl3anc ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ On )
197 196 174 syl ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → Ord ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } )
198 nodmord ⊢ ( 𝑆 ∈ No → Ord dom 𝑆 )
199 71 72 198 3syl ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → Ord dom 𝑆 )
200 ordtri2or ⊢ ( ( Ord ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∧ Ord dom 𝑆 ) → ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ∨ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
201 197 199 200 syl2anc ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ∨ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
202 139 194 201 mpjaodan ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝑍 <s 𝑏 )
203 202 ex ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → ( 𝑍 ≠ 𝑏 → 𝑍 <s 𝑏 ) )
204 56 203 biimtrrid ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → ( ¬ 𝑍 = 𝑏 → 𝑍 <s 𝑏 ) )
205 55 204 mpd ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → 𝑍 <s 𝑏 )
206 205 expr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 → 𝑍 <s 𝑏 ) )
207 9 206 sylbid ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑏 → 𝑍 <s 𝑏 ) )
208 207 ralimdva ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) → ( ∀ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑏 → ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) )
209 3 208 biimtrid ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) → ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) )
210 209 3impia ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 )