Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sltres Structured version   Visualization version   GIF version

Theorem sltres 33243
Description: If the restrictions of two surreals to a given ordinal obey surreal less than, then so do the two surreals themselves. (Contributed by Scott Fenton, 4-Sep-2011.)
Assertion
Ref Expression
sltres ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((𝐴𝑋) <s (𝐵𝑋) → 𝐴 <s 𝐵))

Proof of Theorem sltres
Dummy variables 𝑎 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 noreson 33241 . . . . . . 7 ((𝐴 No 𝑋 ∈ On) → (𝐴𝑋) ∈ No )
213adant2 1128 . . . . . 6 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (𝐴𝑋) ∈ No )
3 noreson 33241 . . . . . . 7 ((𝐵 No 𝑋 ∈ On) → (𝐵𝑋) ∈ No )
433adant1 1127 . . . . . 6 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (𝐵𝑋) ∈ No )
5 sltintdifex 33242 . . . . . . 7 (((𝐴𝑋) ∈ No ∧ (𝐵𝑋) ∈ No ) → ((𝐴𝑋) <s (𝐵𝑋) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ V))
6 onintrab 7501 . . . . . . 7 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ V ↔ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On)
75, 6syl6ib 254 . . . . . 6 (((𝐴𝑋) ∈ No ∧ (𝐵𝑋) ∈ No ) → ((𝐴𝑋) <s (𝐵𝑋) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On))
82, 4, 7syl2anc 587 . . . . 5 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((𝐴𝑋) <s (𝐵𝑋) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On))
98imp 410 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On)
10 simpl3 1190 . . . . . . . 8 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → 𝑋 ∈ On)
11 sltval2 33237 . . . . . . . . . . . 12 (((𝐴𝑋) ∈ No ∧ (𝐵𝑋) ∈ No ) → ((𝐴𝑋) <s (𝐵𝑋) ↔ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)})))
122, 4, 11syl2anc 587 . . . . . . . . . . 11 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((𝐴𝑋) <s (𝐵𝑋) ↔ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)})))
13 fvex 6665 . . . . . . . . . . . . 13 ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ V
14 fvex 6665 . . . . . . . . . . . . 13 ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ V
1513, 14brtp 33059 . . . . . . . . . . . 12 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ↔ ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) ∨ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) ∨ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o)))
16 1n0 8106 . . . . . . . . . . . . . . . . . 18 1o ≠ ∅
1716neii 3013 . . . . . . . . . . . . . . . . 17 ¬ 1o = ∅
18 eqeq1 2826 . . . . . . . . . . . . . . . . 17 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o → (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ↔ 1o = ∅))
1917, 18mtbiri 330 . . . . . . . . . . . . . . . 16 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o → ¬ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
20 ndmfv 6682 . . . . . . . . . . . . . . . 16 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
2119, 20nsyl2 143 . . . . . . . . . . . . . . 15 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋))
2221adantr 484 . . . . . . . . . . . . . 14 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋))
2322orcd 870 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
2421adantr 484 . . . . . . . . . . . . . 14 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋))
2524orcd 870 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
26 2on 8098 . . . . . . . . . . . . . . . . . . . . 21 2o ∈ On
2726elexi 3488 . . . . . . . . . . . . . . . . . . . 20 2o ∈ V
2827prid2 4673 . . . . . . . . . . . . . . . . . . 19 2o ∈ {1o, 2o}
2928nosgnn0i 33240 . . . . . . . . . . . . . . . . . 18 ∅ ≠ 2o
3029neii 3013 . . . . . . . . . . . . . . . . 17 ¬ ∅ = 2o
31 eqeq1 2826 . . . . . . . . . . . . . . . . . 18 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o → (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ↔ 2o = ∅))
32 eqcom 2829 . . . . . . . . . . . . . . . . . 18 (2o = ∅ ↔ ∅ = 2o)
3331, 32syl6bb 290 . . . . . . . . . . . . . . . . 17 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o → (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ↔ ∅ = 2o))
3430, 33mtbiri 330 . . . . . . . . . . . . . . . 16 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o → ¬ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
35 ndmfv 6682 . . . . . . . . . . . . . . . 16 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
3634, 35nsyl2 143 . . . . . . . . . . . . . . 15 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋))
3736adantl 485 . . . . . . . . . . . . . 14 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋))
3837olcd 871 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
3923, 25, 383jaoi 1424 . . . . . . . . . . . 12 (((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) ∨ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) ∨ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o)) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
4015, 39sylbi 220 . . . . . . . . . . 11 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
4112, 40syl6bi 256 . . . . . . . . . 10 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((𝐴𝑋) <s (𝐵𝑋) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋))))
4241imp 410 . . . . . . . . 9 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
43 dmres 5853 . . . . . . . . . . . 12 dom (𝐴𝑋) = (𝑋 ∩ dom 𝐴)
4443elin2 4148 . . . . . . . . . . 11 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ↔ ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐴))
4544simplbi 501 . . . . . . . . . 10 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋)
46 dmres 5853 . . . . . . . . . . . 12 dom (𝐵𝑋) = (𝑋 ∩ dom 𝐵)
4746elin2 4148 . . . . . . . . . . 11 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) ↔ ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐵))
4847simplbi 501 . . . . . . . . . 10 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋)
4945, 48jaoi 854 . . . . . . . . 9 (( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋)
5042, 49syl 17 . . . . . . . 8 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋)
51 onelss 6211 . . . . . . . 8 (𝑋 ∈ On → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ⊆ 𝑋))
5210, 50, 51sylc 65 . . . . . . 7 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ⊆ 𝑋)
5352sselda 3942 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → 𝑦𝑋)
54 onelon 6194 . . . . . . . . 9 (( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → 𝑦 ∈ On)
559, 54sylan 583 . . . . . . . 8 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → 𝑦 ∈ On)
56 intss1 4866 . . . . . . . . . . . . 13 (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ⊆ 𝑦)
57 ontri1 6203 . . . . . . . . . . . . 13 (( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ⊆ 𝑦 ↔ ¬ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
5856, 57syl5ib 247 . . . . . . . . . . . 12 (( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → ¬ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
5958con2d 136 . . . . . . . . . . 11 (( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
609, 59sylan 583 . . . . . . . . . 10 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 ∈ On) → (𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
6160impancom 455 . . . . . . . . 9 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → (𝑦 ∈ On → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
6255, 61mpd 15 . . . . . . . 8 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)})
63 fveq2 6652 . . . . . . . . . . . 12 (𝑎 = 𝑦 → ((𝐴𝑋)‘𝑎) = ((𝐴𝑋)‘𝑦))
64 fveq2 6652 . . . . . . . . . . . 12 (𝑎 = 𝑦 → ((𝐵𝑋)‘𝑎) = ((𝐵𝑋)‘𝑦))
6563, 64neeq12d 3072 . . . . . . . . . . 11 (𝑎 = 𝑦 → (((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎) ↔ ((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦)))
6665elrab 3655 . . . . . . . . . 10 (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ↔ (𝑦 ∈ On ∧ ((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦)))
6766simplbi2 504 . . . . . . . . 9 (𝑦 ∈ On → (((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦) → 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
6867con3d 155 . . . . . . . 8 (𝑦 ∈ On → (¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → ¬ ((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦)))
6955, 62, 68sylc 65 . . . . . . 7 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → ¬ ((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦))
70 df-ne 3012 . . . . . . . 8 (((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦) ↔ ¬ ((𝐴𝑋)‘𝑦) = ((𝐵𝑋)‘𝑦))
7170con2bii 361 . . . . . . 7 (((𝐴𝑋)‘𝑦) = ((𝐵𝑋)‘𝑦) ↔ ¬ ((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦))
7269, 71sylibr 237 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → ((𝐴𝑋)‘𝑦) = ((𝐵𝑋)‘𝑦))
73 fvres 6671 . . . . . . . 8 (𝑦𝑋 → ((𝐴𝑋)‘𝑦) = (𝐴𝑦))
74 fvres 6671 . . . . . . . 8 (𝑦𝑋 → ((𝐵𝑋)‘𝑦) = (𝐵𝑦))
7573, 74eqeq12d 2838 . . . . . . 7 (𝑦𝑋 → (((𝐴𝑋)‘𝑦) = ((𝐵𝑋)‘𝑦) ↔ (𝐴𝑦) = (𝐵𝑦)))
7675biimpd 232 . . . . . 6 (𝑦𝑋 → (((𝐴𝑋)‘𝑦) = ((𝐵𝑋)‘𝑦) → (𝐴𝑦) = (𝐵𝑦)))
7753, 72, 76sylc 65 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → (𝐴𝑦) = (𝐵𝑦))
7877ralrimiva 3174 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → ∀𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} (𝐴𝑦) = (𝐵𝑦))
79 fvresval 33084 . . . . . . . . . . . . . . 15 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∨ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
8079ori 858 . . . . . . . . . . . . . 14 (¬ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
8119, 80nsyl2 143 . . . . . . . . . . . . 13 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
8281eqcomd 2828 . . . . . . . . . . . 12 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
83 eqeq2 2834 . . . . . . . . . . . 12 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o → ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ↔ (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o))
8482, 83mpbid 235 . . . . . . . . . . 11 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o)
8584adantr 484 . . . . . . . . . 10 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o)
8685a1i 11 . . . . . . . . 9 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o))
8721ad2antrl 727 . . . . . . . . . . . . 13 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋))
8887, 45syl 17 . . . . . . . . . . . 12 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋)
89 nofun 33230 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑋) ∈ No → Fun (𝐵𝑋))
90 fvelrn 6826 . . . . . . . . . . . . . . . . . . 19 ((Fun (𝐵𝑋) ∧ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐵𝑋))
9190ex 416 . . . . . . . . . . . . . . . . . 18 (Fun (𝐵𝑋) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐵𝑋)))
9289, 91syl 17 . . . . . . . . . . . . . . . . 17 ((𝐵𝑋) ∈ No → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐵𝑋)))
93 norn 33232 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑋) ∈ No → ran (𝐵𝑋) ⊆ {1o, 2o})
9493sseld 3941 . . . . . . . . . . . . . . . . 17 ((𝐵𝑋) ∈ No → (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐵𝑋) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1o, 2o}))
9592, 94syld 47 . . . . . . . . . . . . . . . 16 ((𝐵𝑋) ∈ No → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1o, 2o}))
96 nosgnn0 33239 . . . . . . . . . . . . . . . . 17 ¬ ∅ ∈ {1o, 2o}
97 eleq1 2901 . . . . . . . . . . . . . . . . 17 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1o, 2o} ↔ ∅ ∈ {1o, 2o}))
9896, 97mtbiri 330 . . . . . . . . . . . . . . . 16 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → ¬ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1o, 2o})
9995, 98nsyli 160 . . . . . . . . . . . . . . 15 ((𝐵𝑋) ∈ No → (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
1004, 99syl 17 . . . . . . . . . . . . . 14 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
101100imp 410 . . . . . . . . . . . . 13 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋))
102101adantrl 715 . . . . . . . . . . . 12 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋))
10347simplbi2 504 . . . . . . . . . . . . 13 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
104103con3d 155 . . . . . . . . . . . 12 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 → (¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐵))
10588, 102, 104sylc 65 . . . . . . . . . . 11 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐵)
106 ndmfv 6682 . . . . . . . . . . 11 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐵 → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
107105, 106syl 17 . . . . . . . . . 10 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)) → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
108107ex 416 . . . . . . . . 9 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅))
10986, 108jcad 516 . . . . . . . 8 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)))
110 fvresval 33084 . . . . . . . . . . . . . 14 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∨ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
111110ori 858 . . . . . . . . . . . . 13 (¬ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
11234, 111nsyl2 143 . . . . . . . . . . . 12 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
113112eqcomd 2828 . . . . . . . . . . 11 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
114 eqeq2 2834 . . . . . . . . . . 11 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o → ((𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ↔ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o))
115113, 114mpbid 235 . . . . . . . . . 10 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o)
11684, 115anim12i 615 . . . . . . . . 9 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) → ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o))
117116a1i 11 . . . . . . . 8 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) → ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o)))
11836ad2antll 728 . . . . . . . . . . . . 13 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋))
119118, 48syl 17 . . . . . . . . . . . 12 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋)
120 nofun 33230 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑋) ∈ No → Fun (𝐴𝑋))
121 fvelrn 6826 . . . . . . . . . . . . . . . . . . 19 ((Fun (𝐴𝑋) ∧ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋)) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐴𝑋))
122121ex 416 . . . . . . . . . . . . . . . . . 18 (Fun (𝐴𝑋) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐴𝑋)))
123120, 122syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴𝑋) ∈ No → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐴𝑋)))
124 norn 33232 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑋) ∈ No → ran (𝐴𝑋) ⊆ {1o, 2o})
125124sseld 3941 . . . . . . . . . . . . . . . . 17 ((𝐴𝑋) ∈ No → (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐴𝑋) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1o, 2o}))
126123, 125syld 47 . . . . . . . . . . . . . . . 16 ((𝐴𝑋) ∈ No → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1o, 2o}))
127 eleq1 2901 . . . . . . . . . . . . . . . . 17 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1o, 2o} ↔ ∅ ∈ {1o, 2o}))
12896, 127mtbiri 330 . . . . . . . . . . . . . . . 16 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → ¬ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1o, 2o})
129126, 128nsyli 160 . . . . . . . . . . . . . . 15 ((𝐴𝑋) ∈ No → (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋)))
1302, 129syl 17 . . . . . . . . . . . . . 14 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋)))
131130imp 410 . . . . . . . . . . . . 13 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋))
132131adantrr 716 . . . . . . . . . . . 12 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o)) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋))
13344simplbi2 504 . . . . . . . . . . . . 13 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋)))
134133con3d 155 . . . . . . . . . . . 12 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 → (¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐴))
135119, 132, 134sylc 65 . . . . . . . . . . 11 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o)) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐴)
136135ex 416 . . . . . . . . . 10 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐴))
137 ndmfv 6682 . . . . . . . . . 10 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐴 → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
138136, 137syl6 35 . . . . . . . . 9 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅))
139115adantl 485 . . . . . . . . . 10 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o)
140139a1i 11 . . . . . . . . 9 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o))
141138, 140jcad 516 . . . . . . . 8 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) → ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o)))
142109, 117, 1413orim123d 1441 . . . . . . 7 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) ∨ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) ∨ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o)) → (((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) ∨ ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o))))
143 fvex 6665 . . . . . . . 8 (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ V
144 fvex 6665 . . . . . . . 8 (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ V
145143, 144brtp 33059 . . . . . . 7 ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ↔ (((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o) ∨ ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2o)))
146142, 15, 1453imtr4g 299 . . . . . 6 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)})))
14712, 146sylbid 243 . . . . 5 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((𝐴𝑋) <s (𝐵𝑋) → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)})))
148147imp 410 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
149 raleq 3386 . . . . . 6 (𝑥 = {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ↔ ∀𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} (𝐴𝑦) = (𝐵𝑦)))
150 fveq2 6652 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → (𝐴𝑥) = (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
151 fveq2 6652 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → (𝐵𝑥) = (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
152150, 151breq12d 5055 . . . . . 6 (𝑥 = {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) ↔ (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)})))
153149, 152anbi12d 633 . . . . 5 (𝑥 = {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) ↔ (∀𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))))
154153rspcev 3598 . . . 4 (( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
1559, 78, 148, 154syl12anc 835 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
156 sltval 33228 . . . . 5 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
1571563adant3 1129 . . . 4 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
158157adantr 484 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
159155, 158mpbird 260 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → 𝐴 <s 𝐵)
160159ex 416 1 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((𝐴𝑋) <s (𝐵𝑋) → 𝐴 <s 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3o 1083  w3a 1084   = wceq 1538  wcel 2114  wne 3011  wral 3130  wrex 3131  {crab 3134  Vcvv 3469  wss 3908  c0 4265  {cpr 4541  {ctp 4543  cop 4545   cint 4851   class class class wbr 5042  dom cdm 5532  ran crn 5533  cres 5534  Oncon0 6169  Fun wfun 6328  cfv 6334  1oc1o 8082  2oc2o 8083   No csur 33221   <s cslt 33222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-ord 6172  df-on 6173  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-1o 8089  df-2o 8090  df-no 33224  df-slt 33225
This theorem is referenced by:  noresle  33274  nosupbnd1lem1  33282  nosupbnd1lem2  33283  nosupbnd1  33288  nosupbnd2lem1  33289  nosupbnd2  33290  noetalem2  33292  noetalem3  33293
  Copyright terms: Public domain W3C validator