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

Theorem sltres 31571
 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 31567 . . . . . . 7 ((𝐴 No 𝑋 ∈ On) → (𝐴𝑋) ∈ No )
213adant2 1078 . . . . . 6 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (𝐴𝑋) ∈ No )
3 noreson 31567 . . . . . . 7 ((𝐵 No 𝑋 ∈ On) → (𝐵𝑋) ∈ No )
433adant1 1077 . . . . . 6 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (𝐵𝑋) ∈ No )
5 sltintdifex 31570 . . . . . . 7 (((𝐴𝑋) ∈ No ∧ (𝐵𝑋) ∈ No ) → ((𝐴𝑋) <s (𝐵𝑋) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ V))
6 onintrab 6963 . . . . . . 7 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ V ↔ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On)
75, 6syl6ib 241 . . . . . 6 (((𝐴𝑋) ∈ No ∧ (𝐵𝑋) ∈ No ) → ((𝐴𝑋) <s (𝐵𝑋) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On))
82, 4, 7syl2anc 692 . . . . 5 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((𝐴𝑋) <s (𝐵𝑋) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On))
98imp 445 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On)
10 simpl3 1064 . . . . . . . 8 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → 𝑋 ∈ On)
11 sltval2 31563 . . . . . . . . . . . 12 (((𝐴𝑋) ∈ No ∧ (𝐵𝑋) ∈ No ) → ((𝐴𝑋) <s (𝐵𝑋) ↔ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)})))
122, 4, 11syl2anc 692 . . . . . . . . . . 11 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((𝐴𝑋) <s (𝐵𝑋) ↔ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)})))
13 fvex 6168 . . . . . . . . . . . . 13 ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ V
14 fvex 6168 . . . . . . . . . . . . 13 ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ V
1513, 14brtp 31400 . . . . . . . . . . . 12 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ↔ ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) ∨ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) ∨ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜)))
16 1n0 7535 . . . . . . . . . . . . . . . . . 18 1𝑜 ≠ ∅
1716neii 2792 . . . . . . . . . . . . . . . . 17 ¬ 1𝑜 = ∅
18 eqeq1 2625 . . . . . . . . . . . . . . . . 17 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 → (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ↔ 1𝑜 = ∅))
1917, 18mtbiri 317 . . . . . . . . . . . . . . . 16 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 → ¬ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
20 ndmfv 6185 . . . . . . . . . . . . . . . 16 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
2119, 20nsyl2 142 . . . . . . . . . . . . . . 15 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋))
2221adantr 481 . . . . . . . . . . . . . 14 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋))
2322orcd 407 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
2421adantr 481 . . . . . . . . . . . . . 14 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋))
2524orcd 407 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
26 2on 7528 . . . . . . . . . . . . . . . . . . . . 21 2𝑜 ∈ On
2726elexi 3203 . . . . . . . . . . . . . . . . . . . 20 2𝑜 ∈ V
2827prid2 4275 . . . . . . . . . . . . . . . . . . 19 2𝑜 ∈ {1𝑜, 2𝑜}
2928nosgnn0i 31566 . . . . . . . . . . . . . . . . . 18 ∅ ≠ 2𝑜
3029neii 2792 . . . . . . . . . . . . . . . . 17 ¬ ∅ = 2𝑜
31 eqeq1 2625 . . . . . . . . . . . . . . . . . 18 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜 → (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ↔ 2𝑜 = ∅))
32 eqcom 2628 . . . . . . . . . . . . . . . . . 18 (2𝑜 = ∅ ↔ ∅ = 2𝑜)
3331, 32syl6bb 276 . . . . . . . . . . . . . . . . 17 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜 → (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ↔ ∅ = 2𝑜))
3430, 33mtbiri 317 . . . . . . . . . . . . . . . 16 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜 → ¬ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
35 ndmfv 6185 . . . . . . . . . . . . . . . 16 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
3634, 35nsyl2 142 . . . . . . . . . . . . . . 15 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋))
3736adantl 482 . . . . . . . . . . . . . 14 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋))
3837olcd 408 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
3923, 25, 383jaoi 1388 . . . . . . . . . . . 12 (((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) ∨ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) ∨ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜)) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
4015, 39sylbi 207 . . . . . . . . . . 11 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
4112, 40syl6bi 243 . . . . . . . . . 10 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((𝐴𝑋) <s (𝐵𝑋) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋))))
4241imp 445 . . . . . . . . 9 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
43 dmres 5388 . . . . . . . . . . . 12 dom (𝐴𝑋) = (𝑋 ∩ dom 𝐴)
4443elin2 3785 . . . . . . . . . . 11 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ↔ ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐴))
4544simplbi 476 . . . . . . . . . 10 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋)
46 dmres 5388 . . . . . . . . . . . 12 dom (𝐵𝑋) = (𝑋 ∩ dom 𝐵)
4746elin2 3785 . . . . . . . . . . 11 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) ↔ ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐵))
4847simplbi 476 . . . . . . . . . 10 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋)
4945, 48jaoi 394 . . . . . . . . 9 (( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) ∨ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋)
5042, 49syl 17 . . . . . . . 8 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋)
51 onelss 5735 . . . . . . . 8 (𝑋 ∈ On → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ⊆ 𝑋))
5210, 50, 51sylc 65 . . . . . . 7 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ⊆ 𝑋)
5352sselda 3588 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → 𝑦𝑋)
54 onelon 5717 . . . . . . . . 9 (( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → 𝑦 ∈ On)
559, 54sylan 488 . . . . . . . 8 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → 𝑦 ∈ On)
56 intss1 4464 . . . . . . . . . . . . 13 (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ⊆ 𝑦)
57 ontri1 5726 . . . . . . . . . . . . 13 (( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ⊆ 𝑦 ↔ ¬ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
5856, 57syl5ib 234 . . . . . . . . . . . 12 (( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → ¬ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
5958con2d 129 . . . . . . . . . . 11 (( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
609, 59sylan 488 . . . . . . . . . 10 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 ∈ On) → (𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
6160impancom 456 . . . . . . . . 9 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → (𝑦 ∈ On → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
6255, 61mpd 15 . . . . . . . 8 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)})
63 fveq2 6158 . . . . . . . . . . . 12 (𝑎 = 𝑦 → ((𝐴𝑋)‘𝑎) = ((𝐴𝑋)‘𝑦))
64 fveq2 6158 . . . . . . . . . . . 12 (𝑎 = 𝑦 → ((𝐵𝑋)‘𝑎) = ((𝐵𝑋)‘𝑦))
6563, 64neeq12d 2851 . . . . . . . . . . 11 (𝑎 = 𝑦 → (((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎) ↔ ((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦)))
6665elrab 3351 . . . . . . . . . 10 (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ↔ (𝑦 ∈ On ∧ ((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦)))
6766simplbi2 654 . . . . . . . . 9 (𝑦 ∈ On → (((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦) → 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
6867con3d 148 . . . . . . . 8 (𝑦 ∈ On → (¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → ¬ ((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦)))
6955, 62, 68sylc 65 . . . . . . 7 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → ¬ ((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦))
70 df-ne 2791 . . . . . . . 8 (((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦) ↔ ¬ ((𝐴𝑋)‘𝑦) = ((𝐵𝑋)‘𝑦))
7170con2bii 347 . . . . . . 7 (((𝐴𝑋)‘𝑦) = ((𝐵𝑋)‘𝑦) ↔ ¬ ((𝐴𝑋)‘𝑦) ≠ ((𝐵𝑋)‘𝑦))
7269, 71sylibr 224 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → ((𝐴𝑋)‘𝑦) = ((𝐵𝑋)‘𝑦))
73 fvres 6174 . . . . . . . 8 (𝑦𝑋 → ((𝐴𝑋)‘𝑦) = (𝐴𝑦))
74 fvres 6174 . . . . . . . 8 (𝑦𝑋 → ((𝐵𝑋)‘𝑦) = (𝐵𝑦))
7573, 74eqeq12d 2636 . . . . . . 7 (𝑦𝑋 → (((𝐴𝑋)‘𝑦) = ((𝐵𝑋)‘𝑦) ↔ (𝐴𝑦) = (𝐵𝑦)))
7675biimpd 219 . . . . . 6 (𝑦𝑋 → (((𝐴𝑋)‘𝑦) = ((𝐵𝑋)‘𝑦) → (𝐴𝑦) = (𝐵𝑦)))
7753, 72, 76sylc 65 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) ∧ 𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → (𝐴𝑦) = (𝐵𝑦))
7877ralrimiva 2962 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → ∀𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} (𝐴𝑦) = (𝐵𝑦))
79 fvresval 31422 . . . . . . . . . . . . . . 15 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∨ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
8079ori 390 . . . . . . . . . . . . . 14 (¬ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
8119, 80nsyl2 142 . . . . . . . . . . . . 13 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
8281eqcomd 2627 . . . . . . . . . . . 12 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
83 eqeq2 2632 . . . . . . . . . . . 12 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 → ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ↔ (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜))
8482, 83mpbid 222 . . . . . . . . . . 11 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜)
8584adantr 481 . . . . . . . . . 10 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜)
8685a1i 11 . . . . . . . . 9 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜))
8721ad2antrl 763 . . . . . . . . . . . . 13 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋))
8887, 45syl 17 . . . . . . . . . . . 12 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋)
89 nofun 31556 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑋) ∈ No → Fun (𝐵𝑋))
90 fvelrn 6318 . . . . . . . . . . . . . . . . . . 19 ((Fun (𝐵𝑋) ∧ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐵𝑋))
9190ex 450 . . . . . . . . . . . . . . . . . 18 (Fun (𝐵𝑋) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐵𝑋)))
9289, 91syl 17 . . . . . . . . . . . . . . . . 17 ((𝐵𝑋) ∈ No → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐵𝑋)))
93 norn 31558 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑋) ∈ No → ran (𝐵𝑋) ⊆ {1𝑜, 2𝑜})
9493sseld 3587 . . . . . . . . . . . . . . . . 17 ((𝐵𝑋) ∈ No → (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐵𝑋) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1𝑜, 2𝑜}))
9592, 94syld 47 . . . . . . . . . . . . . . . 16 ((𝐵𝑋) ∈ No → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1𝑜, 2𝑜}))
96 nosgnn0 31565 . . . . . . . . . . . . . . . . 17 ¬ ∅ ∈ {1𝑜, 2𝑜}
97 eleq1 2686 . . . . . . . . . . . . . . . . 17 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1𝑜, 2𝑜} ↔ ∅ ∈ {1𝑜, 2𝑜}))
9896, 97mtbiri 317 . . . . . . . . . . . . . . . 16 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → ¬ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1𝑜, 2𝑜})
9995, 98nsyli 155 . . . . . . . . . . . . . . 15 ((𝐵𝑋) ∈ No → (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
1004, 99syl 17 . . . . . . . . . . . . . 14 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
101100imp 445 . . . . . . . . . . . . 13 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋))
102101adantrl 751 . . . . . . . . . . . 12 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋))
10347simplbi2 654 . . . . . . . . . . . . 13 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋)))
104103con3d 148 . . . . . . . . . . . 12 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 → (¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐵))
10588, 102, 104sylc 65 . . . . . . . . . . 11 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐵)
106 ndmfv 6185 . . . . . . . . . . 11 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐵 → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
107105, 106syl 17 . . . . . . . . . 10 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)) → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
108107ex 450 . . . . . . . . 9 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅))
10986, 108jcad 555 . . . . . . . 8 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)))
110 fvresval 31422 . . . . . . . . . . . . . 14 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∨ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
111110ori 390 . . . . . . . . . . . . 13 (¬ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
11234, 111nsyl2 142 . . . . . . . . . . . 12 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜 → ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
113112eqcomd 2627 . . . . . . . . . . 11 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜 → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
114 eqeq2 2632 . . . . . . . . . . 11 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜 → ((𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ↔ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜))
115113, 114mpbid 222 . . . . . . . . . 10 (((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜 → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜)
11684, 115anim12i 589 . . . . . . . . 9 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) → ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜))
117116a1i 11 . . . . . . . 8 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) → ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜)))
11836ad2antll 764 . . . . . . . . . . . . 13 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐵𝑋))
119118, 48syl 17 . . . . . . . . . . . 12 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜)) → {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋)
120 nofun 31556 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑋) ∈ No → Fun (𝐴𝑋))
121 fvelrn 6318 . . . . . . . . . . . . . . . . . . 19 ((Fun (𝐴𝑋) ∧ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋)) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐴𝑋))
122121ex 450 . . . . . . . . . . . . . . . . . 18 (Fun (𝐴𝑋) → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐴𝑋)))
123120, 122syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴𝑋) ∈ No → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐴𝑋)))
124 norn 31558 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑋) ∈ No → ran (𝐴𝑋) ⊆ {1𝑜, 2𝑜})
125124sseld 3587 . . . . . . . . . . . . . . . . 17 ((𝐴𝑋) ∈ No → (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ ran (𝐴𝑋) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1𝑜, 2𝑜}))
126123, 125syld 47 . . . . . . . . . . . . . . . 16 ((𝐴𝑋) ∈ No → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) → ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1𝑜, 2𝑜}))
127 eleq1 2686 . . . . . . . . . . . . . . . . 17 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1𝑜, 2𝑜} ↔ ∅ ∈ {1𝑜, 2𝑜}))
12896, 127mtbiri 317 . . . . . . . . . . . . . . . 16 (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → ¬ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ {1𝑜, 2𝑜})
129126, 128nsyli 155 . . . . . . . . . . . . . . 15 ((𝐴𝑋) ∈ No → (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋)))
1302, 129syl 17 . . . . . . . . . . . . . 14 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋)))
131130imp 445 . . . . . . . . . . . . 13 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋))
132131adantrr 752 . . . . . . . . . . . 12 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜)) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋))
13344simplbi2 654 . . . . . . . . . . . . 13 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 → ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋)))
134133con3d 148 . . . . . . . . . . . 12 ( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ 𝑋 → (¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom (𝐴𝑋) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐴))
135119, 132, 134sylc 65 . . . . . . . . . . 11 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜)) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐴)
136135ex 450 . . . . . . . . . 10 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) → ¬ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐴))
137 ndmfv 6185 . . . . . . . . . 10 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ dom 𝐴 → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅)
138136, 137syl6 35 . . . . . . . . 9 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅))
139115adantl 482 . . . . . . . . . 10 ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜)
140139a1i 11 . . . . . . . . 9 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) → (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜))
141138, 140jcad 555 . . . . . . . 8 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) → ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜)))
142109, 117, 1413orim123d 1404 . . . . . . 7 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (((((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) ∨ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) ∨ (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜)) → (((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) ∨ ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜))))
143 fvex 6168 . . . . . . . 8 (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ V
144 fvex 6168 . . . . . . . 8 (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ∈ V
145143, 144brtp 31400 . . . . . . 7 ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) ↔ (((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜) ∨ ((𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) = 2𝑜)))
146142, 15, 1453imtr4g 285 . . . . . 6 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (((𝐴𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐵𝑋)‘ {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}) → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)})))
14712, 146sylbid 230 . . . . 5 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((𝐴𝑋) <s (𝐵𝑋) → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)})))
148147imp 445 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
149 raleq 3131 . . . . . 6 (𝑥 = {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ↔ ∀𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} (𝐴𝑦) = (𝐵𝑦)))
150 fveq2 6158 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → (𝐴𝑥) = (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
151 fveq2 6158 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → (𝐵𝑥) = (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))
152150, 151breq12d 4636 . . . . . 6 (𝑥 = {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)})))
153149, 152anbi12d 746 . . . . 5 (𝑥 = {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} → ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) ↔ (∀𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))))
154153rspcev 3299 . . . 4 (( {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ ((𝐴𝑋)‘𝑎) ≠ ((𝐵𝑋)‘𝑎)}))) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
1559, 78, 148, 154syl12anc 1321 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
156 sltval 31554 . . . . 5 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
1571563adant3 1079 . . . 4 ((𝐴 No 𝐵 No 𝑋 ∈ On) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
158157adantr 481 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
159155, 158mpbird 247 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ (𝐴𝑋) <s (𝐵𝑋)) → 𝐴 <s 𝐵)
160159ex 450 1 ((𝐴 No 𝐵 No 𝑋 ∈ On) → ((𝐴𝑋) <s (𝐵𝑋) → 𝐴 <s 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∨ w3o 1035   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∀wral 2908  ∃wrex 2909  {crab 2912  Vcvv 3190   ⊆ wss 3560  ∅c0 3897  {cpr 4157  {ctp 4159  ⟨cop 4161  ∩ cint 4447   class class class wbr 4623  dom cdm 5084  ran crn 5085   ↾ cres 5086  Oncon0 5692  Fun wfun 5851  ‘cfv 5857  1𝑜c1o 7513  2𝑜c2o 7514   No csur 31547
 Copyright terms: Public domain W3C validator