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 sseldi ⊢ ( ( ( ( 𝐴 ⊆ 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 incom ⊢ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ∩ dom 𝑆 ) = ( dom 𝑆 ∩ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) )
64 disjdif ⊢ ( dom 𝑆 ∩ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ) = ∅
65 63 64 eqtri ⊢ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ∩ dom 𝑆 ) = ∅
66 xpdisj1 ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ∩ dom 𝑆 ) = ∅ → ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ∩ ( dom 𝑆 × V ) ) = ∅ )
67 65 66 ax-mp ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ∩ ( dom 𝑆 × V ) ) = ∅
68 62 67 eqtri ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) = ∅
69 68 uneq2i ⊢ ( ( 𝑆 ↾ dom 𝑆 ) ∪ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) ) = ( ( 𝑆 ↾ dom 𝑆 ) ∪ ∅ )
70 un0 ⊢ ( ( 𝑆 ↾ dom 𝑆 ) ∪ ∅ ) = ( 𝑆 ↾ dom 𝑆 )
71 69 70 eqtri ⊢ ( ( 𝑆 ↾ dom 𝑆 ) ∪ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) ) = ( 𝑆 ↾ dom 𝑆 )
72 60 61 71 3eqtri ⊢ ( 𝑍 ↾ dom 𝑆 ) = ( 𝑆 ↾ dom 𝑆 )
73 simplll ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
74 1 nosupno ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No )
75 73 74 syl ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝑆 ∈ No )
76 75 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → 𝑆 ∈ No )
77 nofun ⊢ ( 𝑆 ∈ No → Fun 𝑆 )
78 76 77 syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → Fun 𝑆 )
79 funrel ⊢ ( Fun 𝑆 → Rel 𝑆 )
80 resdm ⊢ ( Rel 𝑆 → ( 𝑆 ↾ dom 𝑆 ) = 𝑆 )
81 78 79 80 3syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑆 ↾ dom 𝑆 ) = 𝑆 )
82 72 81 syl5eq ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑍 ↾ dom 𝑆 ) = 𝑆 )
83 82 fveq1d ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑍 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
84 59 83 eqtr3d ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
85 simp-4l ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝐴 ⊆ No )
86 simp-4r ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝐴 ∈ V )
87 simplrr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → 𝐵 ∈ V )
88 87 adantr ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝐵 ∈ V )
89 1 2 noetasuplem1 ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝑍 ∈ No )
90 85 86 88 89 syl3anc ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝑍 ∈ No )
91 90 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → 𝑍 ∈ No )
92 12 adantr ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝑏 ∈ No )
93 92 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → 𝑏 ∈ No )
94 simplr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → 𝑍 ≠ 𝑏 )
95 nosepne ⊢ ( ( 𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏 ) → ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( 𝑏 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
96 91 93 94 95 syl3anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( 𝑏 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
97 84 96 eqnetrrd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( 𝑏 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
98 58 fvresd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( 𝑏 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
99 97 98 neeqtrrd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
100 fveq2 ⊢ ( 𝑞 = ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } → ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
101 fveq2 ⊢ ( 𝑞 = ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } → ( 𝑆 ‘ 𝑞 ) = ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
102 100 101 neeq12d ⊢ ( 𝑞 = ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } → ( ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) ≠ ( 𝑆 ‘ 𝑞 ) ↔ ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ) )
103 df-ne ⊢ ( ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) ≠ ( 𝑆 ‘ 𝑞 ) ↔ ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) )
104 necom ⊢ ( ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ↔ ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
105 102 103 104 3bitr3g ⊢ ( 𝑞 = ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } → ( ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ↔ ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ) )
106 105 rspcev ⊢ ( ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ∧ ( 𝑆 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ≠ ( ( 𝑏 ↾ dom 𝑆 ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) ) → ∃ 𝑞 ∈ dom 𝑆 ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) )
107 58 99 106 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ∃ 𝑞 ∈ dom 𝑆 ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) )
108 rexeq ⊢ ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 → ( ∃ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ↔ ∃ 𝑞 ∈ dom 𝑆 ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
109 107 108 syl5ibrcom ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 → ∃ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
110 rexnal ⊢ ( ∃ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ¬ ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ↔ ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) )
111 109 110 syl6ib ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 → ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
112 57 111 syl5 ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ¬ ¬ dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 → ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
113 112 orrd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ¬ dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∨ ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
114 nofun ⊢ ( 𝑏 ∈ No → Fun 𝑏 )
115 funres ⊢ ( Fun 𝑏 → Fun ( 𝑏 ↾ dom 𝑆 ) )
116 93 114 115 3syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → Fun ( 𝑏 ↾ dom 𝑆 ) )
117 eqfunfv ⊢ ( ( Fun ( 𝑏 ↾ dom 𝑆 ) ∧ Fun 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ↔ ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∧ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) ) )
118 116 78 117 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ↔ ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∧ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) ) )
119 ianor ⊢ ( ¬ ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∧ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) ↔ ( ¬ dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∨ ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
120 119 con1bii ⊢ ( ¬ ( ¬ dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∨ ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) ↔ ( dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∧ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) )
121 118 120 bitr4di ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ↔ ¬ ( ¬ dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∨ ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) ) )
122 121 con2bid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( ¬ dom ( 𝑏 ↾ dom 𝑆 ) = dom 𝑆 ∨ ¬ ∀ 𝑞 ∈ dom ( 𝑏 ↾ dom 𝑆 ) ( ( 𝑏 ↾ dom 𝑆 ) ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) ↔ ¬ ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ) )
123 113 122 mpbid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ¬ ( 𝑏 ↾ dom 𝑆 ) = 𝑆 )
124 123 pm2.21d ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 → 𝑍 <s 𝑏 ) )
125 82 breq1d ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑍 ↾ dom 𝑆 ) <s ( 𝑏 ↾ dom 𝑆 ) ↔ 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) ) )
126 nodmon ⊢ ( 𝑆 ∈ No → dom 𝑆 ∈ On )
127 76 126 syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → dom 𝑆 ∈ On )
128 sltres ⊢ ( ( 𝑍 ∈ No ∧ 𝑏 ∈ No ∧ dom 𝑆 ∈ On ) → ( ( 𝑍 ↾ dom 𝑆 ) <s ( 𝑏 ↾ dom 𝑆 ) → 𝑍 <s 𝑏 ) )
129 91 93 127 128 syl3anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑍 ↾ dom 𝑆 ) <s ( 𝑏 ↾ dom 𝑆 ) → 𝑍 <s 𝑏 ) )
130 125 129 sylbird ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) → 𝑍 <s 𝑏 ) )
131 simplrr ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 )
132 131 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 )
133 noreson ⊢ ( ( 𝑏 ∈ No ∧ dom 𝑆 ∈ On ) → ( 𝑏 ↾ dom 𝑆 ) ∈ No )
134 93 127 133 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( 𝑏 ↾ dom 𝑆 ) ∈ No )
135 sltso ⊢ <s Or No
136 sotric ⊢ ( ( <s Or No ∧ ( ( 𝑏 ↾ dom 𝑆 ) ∈ No ∧ 𝑆 ∈ No ) ) → ( ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ↔ ¬ ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ∨ 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) ) ) )
137 135 136 mpan ⊢ ( ( ( 𝑏 ↾ dom 𝑆 ) ∈ No ∧ 𝑆 ∈ No ) → ( ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ↔ ¬ ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ∨ 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) ) ) )
138 134 76 137 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ↔ ¬ ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ∨ 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) ) ) )
139 138 con2bid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ∨ 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) ) ↔ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) )
140 132 139 mpbird ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → ( ( 𝑏 ↾ dom 𝑆 ) = 𝑆 ∨ 𝑆 <s ( 𝑏 ↾ dom 𝑆 ) ) )
141 124 130 140 mpjaod ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) → 𝑍 <s 𝑏 )
142 90 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑍 ∈ No )
143 92 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑏 ∈ No )
144 simplr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑍 ≠ 𝑏 )
145 2 fveq1i ⊢ ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } )
146 simp-4l ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
147 146 74 77 3syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → Fun 𝑆 )
148 funfn ⊢ ( Fun 𝑆 ↔ 𝑆 Fn dom 𝑆 )
149 147 148 sylib ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑆 Fn dom 𝑆 )
150 46 fconst ⊢ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) : ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ⟶ { 1o }
151 ffn ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) : ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ⟶ { 1o } → ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) Fn ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) )
152 150 151 ax-mp ⊢ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) Fn ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 )
153 152 a1i ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) Fn ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) )
154 64 a1i ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( dom 𝑆 ∩ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ) = ∅ )
155 necom ⊢ ( ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) ↔ ( 𝑏 ‘ 𝑝 ) ≠ ( 𝑍 ‘ 𝑝 ) )
156 155 rabbii ⊢ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } = { 𝑝 ∈ On ∣ ( 𝑏 ‘ 𝑝 ) ≠ ( 𝑍 ‘ 𝑝 ) }
157 156 inteqi ⊢ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } = ∩ { 𝑝 ∈ On ∣ ( 𝑏 ‘ 𝑝 ) ≠ ( 𝑍 ‘ 𝑝 ) }
158 144 necomd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑏 ≠ 𝑍 )
159 nosepssdm ⊢ ( ( 𝑏 ∈ No ∧ 𝑍 ∈ No ∧ 𝑏 ≠ 𝑍 ) → ∩ { 𝑝 ∈ On ∣ ( 𝑏 ‘ 𝑝 ) ≠ ( 𝑍 ‘ 𝑝 ) } ⊆ dom 𝑏 )
160 143 142 158 159 syl3anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ∩ { 𝑝 ∈ On ∣ ( 𝑏 ‘ 𝑝 ) ≠ ( 𝑍 ‘ 𝑝 ) } ⊆ dom 𝑏 )
161 157 160 eqsstrid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ⊆ dom 𝑏 )
162 143 17 syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( bday ‘ 𝑏 ) = dom 𝑏 )
163 simplrl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → 𝐵 ⊆ No )
164 163 adantr ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝐵 ⊆ No )
165 164 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝐵 ⊆ No )
166 simplrl ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝑏 ∈ 𝐵 )
167 166 adantr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑏 ∈ 𝐵 )
168 165 167 23 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( bday ‘ 𝑏 ) ∈ ( bday “ 𝐵 ) )
169 162 168 eqeltrrd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → dom 𝑏 ∈ ( bday “ 𝐵 ) )
170 169 26 syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵 ) )
171 143 28 36 3syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( dom 𝑏 ⊆ ∪ ( bday “ 𝐵 ) ↔ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) ) )
172 170 171 mpbid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) )
173 nosepon ⊢ ( ( 𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏 ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ On )
174 142 143 144 173 syl3anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ On )
175 eloni ⊢ ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ On → Ord ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } )
176 ordsuc ⊢ ( Ord ∪ ( bday “ 𝐵 ) ↔ Ord suc ∪ ( bday “ 𝐵 ) )
177 34 176 mpbi ⊢ Ord suc ∪ ( bday “ 𝐵 )
178 ordtr2 ⊢ ( ( Ord ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∧ Ord suc ∪ ( bday “ 𝐵 ) ) → ( ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ suc ∪ ( bday “ 𝐵 ) ) )
179 177 178 mpan2 ⊢ ( Ord ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } → ( ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ suc ∪ ( bday “ 𝐵 ) ) )
180 174 175 179 3syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵 ) ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ suc ∪ ( bday “ 𝐵 ) ) )
181 161 172 180 mp2and ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ suc ∪ ( bday “ 𝐵 ) )
182 simpr ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } )
183 146 74 126 3syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → dom 𝑆 ∈ On )
184 ontri1 ⊢ ( ( dom 𝑆 ∈ On ∧ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ On ) → ( dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ↔ ¬ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) )
185 183 174 184 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ↔ ¬ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ) )
186 182 185 mpbid ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ¬ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 )
187 181 186 eldifd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) )
188 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 ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
189 149 153 154 187 188 syl112anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
190 145 189 syl5eq ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
191 46 fvconst2 ⊢ ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) → ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = 1o )
192 187 191 syl ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = 1o )
193 190 192 eqtrd ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = 1o )
194 nosep1o ⊢ ( ( ( 𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏 ) ∧ ( 𝑍 ‘ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) = 1o ) → 𝑍 <s 𝑏 )
195 142 143 144 193 194 syl31anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) ∧ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) → 𝑍 <s 𝑏 )
196 simpr ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝑍 ≠ 𝑏 )
197 90 92 196 173 syl3anc ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ On )
198 197 175 syl ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → Ord ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } )
199 nodmord ⊢ ( 𝑆 ∈ No → Ord dom 𝑆 )
200 73 74 199 3syl ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → Ord dom 𝑆 )
201 ordtri2or ⊢ ( ( Ord ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∧ Ord dom 𝑆 ) → ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ∨ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
202 198 200 201 syl2anc ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → ( ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ∈ dom 𝑆 ∨ dom 𝑆 ⊆ ∩ { 𝑝 ∈ On ∣ ( 𝑍 ‘ 𝑝 ) ≠ ( 𝑏 ‘ 𝑝 ) } ) )
203 141 195 202 mpjaodan ⊢ ( ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) ∧ 𝑍 ≠ 𝑏 ) → 𝑍 <s 𝑏 )
204 203 ex ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → ( 𝑍 ≠ 𝑏 → 𝑍 <s 𝑏 ) )
205 56 204 syl5bir ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → ( ¬ 𝑍 = 𝑏 → 𝑍 <s 𝑏 ) )
206 55 205 mpd ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 ) ) → 𝑍 <s 𝑏 )
207 206 expr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ¬ ( 𝑏 ↾ dom 𝑆 ) <s 𝑆 → 𝑍 <s 𝑏 ) )
208 9 207 sylbid ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑏 → 𝑍 <s 𝑏 ) )
209 208 ralimdva ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) → ( ∀ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑏 → ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) )
210 3 209 syl5bi ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) → ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) )
211 210 3impia ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 )