Theorem ltsres 28024

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
ltsres	⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → 𝐴 <s 𝐵))

Proof of Theorem ltsres

Dummy variables 𝑎 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		noreson 28022	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑋 ∈ On) → (𝐴 ↾ 𝑋) ∈ No)
2	1	3adant2 1149	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐴 ↾ 𝑋) ∈ No)
3		noreson 28022	. . . . . . 7 ⊢ ((𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐵 ↾ 𝑋) ∈ No)
4	3	3adant1 1148	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐵 ↾ 𝑋) ∈ No)
5		ltsintdifex 28023	. . . . . . 7 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ V))
6		onintrab 7810	. . . . . . 7 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ V ↔ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On)
7	5, 6	imbitrdi 254	. . . . . 6 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On))
8	2, 4, 7	syl2anc 596	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On))
9	8	imp 412	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On)
10		simpl3 1212	. . . . . . . 8 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → 𝑋 ∈ On)
11		ltsval2 28018	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) ↔ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
12	2, 4, 11	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) ↔ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
13		fvex 6898	. . . . . . . . . . . . 13 ⊢ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
14		fvex 6898	. . . . . . . . . . . . 13 ⊢ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
15	13, 14	brtp 5496	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
16		1n0 8498	. . . . . . . . . . . . . . . . . 18 ⊢ 1o ≠ ∅
17	16	neii 2957	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1o = ∅
18		eqeq1 2764	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ 1o = ∅))
19	17, 18	mtbiri 330	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ¬ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
20		ndmfv 6917	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
21	19, 20	nsyl2 142	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
22	21	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
23	22	orcd 887	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
24	21	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
25	24	orcd 887	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
26		2on 8493	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2o ∈ On
27	26	elexi 3472	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2o ∈ V
28	27	prid2 4720	. . . . . . . . . . . . . . . . . . 19 ⊢ 2o ∈ {1o, 2o}
29	28	nosgnn0i 28021	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ≠ 2o
30	29	neii 2957	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ∅ = 2o
31		eqeq1 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ 2o = ∅))
32		eqcom 2767	. . . . . . . . . . . . . . . . . 18 ⊢ (2o = ∅ ↔ ∅ = 2o)
33	31, 32	bitrdi 290	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ ∅ = 2o))
34	30, 33	mtbiri 330	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ¬ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
35		ndmfv 6917	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
36	34, 35	nsyl2 142	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
37	36	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
38	37	olcd 888	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
39	23, 25, 38	3jaoi 1454	. . . . . . . . . . . 12 ⊢ (((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
40	15, 39	sylbi 220	. . . . . . . . . . 11 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
41	12, 40	biimtrdi 256	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))))
42	41	imp 412	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
43		dmres 6002	. . . . . . . . . . . 12 ⊢ dom (𝐴 ↾ 𝑋) = (𝑋 ∩ dom 𝐴)
44	43	elin2 4100	. . . . . . . . . . 11 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ↔ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴))
45	44	simplbi 502	. . . . . . . . . 10 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
46		dmres 6002	. . . . . . . . . . . 12 ⊢ dom (𝐵 ↾ 𝑋) = (𝑋 ∩ dom 𝐵)
47	46	elin2 4100	. . . . . . . . . . 11 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) ↔ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵))
48	47	simplbi 502	. . . . . . . . . 10 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
49	45, 48	jaoi 871	. . . . . . . . 9 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
50	42, 49	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
51		onelss 6405	. . . . . . . 8 ⊢ (𝑋 ∈ On → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑋))
52	10, 50, 51	sylc 66	. . . . . . 7 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑋)
53	52	sselda 3908	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ 𝑋)
54		onelon 6387	. . . . . . . . 9 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ On)
55	9, 54	sylan 592	. . . . . . . 8 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ On)
56		intss1 4922	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑦)
57		ontri1 6397	. . . . . . . . . . . . 13 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑦 ↔ ¬ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
58	56, 57	imbitrid 247	. . . . . . . . . . . 12 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
59	58	con2d 135	. . . . . . . . . . 11 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
60	9, 59	sylan 592	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ On) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
61	60	impancom 457	. . . . . . . . 9 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (𝑦 ∈ On → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
62	55, 61	mpd 16	. . . . . . . 8 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})
63		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑦 → ((𝐴 ↾ 𝑋)‘𝑎) = ((𝐴 ↾ 𝑋)‘𝑦))
64		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑦 → ((𝐵 ↾ 𝑋)‘𝑎) = ((𝐵 ↾ 𝑋)‘𝑦))
65	63, 64	neeq12d 3016	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑦 → (((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎) ↔ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦)))
66	65	elrab 3644	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ↔ (𝑦 ∈ On ∧ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦)))
67	66	simplbi2 506	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦) → 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
68	67	con3d 153	. . . . . . . 8 ⊢ (𝑦 ∈ On → (¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦)))
69	55, 62, 68	sylc 66	. . . . . . 7 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ¬ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦))
70		df-ne 2956	. . . . . . . 8 ⊢ (((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦))
71	70	con2bii 360	. . . . . . 7 ⊢ (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦))
72	69, 71	sylibr 237	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦))
73		fvres 6904	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑋 → ((𝐴 ↾ 𝑋)‘𝑦) = (𝐴‘𝑦))
74		fvres 6904	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑋 → ((𝐵 ↾ 𝑋)‘𝑦) = (𝐵‘𝑦))
75	73, 74	eqeq12d 2776	. . . . . . 7 ⊢ (𝑦 ∈ 𝑋 → (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) ↔ (𝐴‘𝑦) = (𝐵‘𝑦)))
76	75	biimpd 232	. . . . . 6 ⊢ (𝑦 ∈ 𝑋 → (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) → (𝐴‘𝑦) = (𝐵‘𝑦)))
77	53, 72, 76	sylc 66	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (𝐴‘𝑦) = (𝐵‘𝑦))
78	77	ralrimiva 3154	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦))
79		fvresval 7368	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∨ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
80	79	ori 875	. . . . . . . . . . . . . 14 ⊢ (¬ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
81	19, 80	nsyl2 142	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
82	81	eqcomd 2766	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
83		eqeq2 2772	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o))
84	82, 83	mpbid 235	. . . . . . . . . . 11 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o)
85	84	adantr 486	. . . . . . . . . 10 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o)
86	85	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o))
87	21	ad2antrl 741	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
88	87, 45	syl 18	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
89		nofun 28011	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ↾ 𝑋) ∈ No → Fun (𝐵 ↾ 𝑋))
90		fvelrn 7076	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun (𝐵 ↾ 𝑋) ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋))
91	90	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun (𝐵 ↾ 𝑋) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋)))
92	89, 91	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋)))
93		norn 28013	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ↾ 𝑋) ∈ No → ran (𝐵 ↾ 𝑋) ⊆ {1o, 2o})
94	93	sseld 3907	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
95	92, 94	syld 48	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
96		nosgnn0 28020	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ∅ ∈ {1o, 2o}
97		eleq1 2848	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o} ↔ ∅ ∈ {1o, 2o}))
98	96, 97	mtbiri 330	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → ¬ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o})
99	95, 98	nsyli 158	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
100	4, 99	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
101	100	imp 412	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
102	101	adantrl 729	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
103	47	simplbi2 506	. . . . . . . . . . . . 13 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵 → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
104	103	con3d 153	. . . . . . . . . . . 12 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 → (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵))
105	88, 102, 104	sylc 66	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵)
106		ndmfv 6917	. . . . . . . . . . 11 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵 → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
107	105, 106	syl 18	. . . . . . . . . 10 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
108	107	ex 418	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅))
109	86, 108	jcad 522	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)))
110		fvresval 7368	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∨ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
111	110	ori 875	. . . . . . . . . . . . 13 ⊢ (¬ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
112	34, 111	nsyl2 142	. . . . . . . . . . . 12 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
113	112	eqcomd 2766	. . . . . . . . . . 11 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
114		eqeq2 2772	. . . . . . . . . . 11 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ((𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o))
115	113, 114	mpbid 235	. . . . . . . . . 10 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)
116	84, 115	anim12i 625	. . . . . . . . 9 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o))
117	116	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
118	36	ad2antll 742	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
119	118, 48	syl 18	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
120		nofun 28011	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ↾ 𝑋) ∈ No → Fun (𝐴 ↾ 𝑋))
121		fvelrn 7076	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun (𝐴 ↾ 𝑋) ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋)) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋))
122	121	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun (𝐴 ↾ 𝑋) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋)))
123	120, 122	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋)))
124		norn 28013	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ↾ 𝑋) ∈ No → ran (𝐴 ↾ 𝑋) ⊆ {1o, 2o})
125	124	sseld 3907	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
126	123, 125	syld 48	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
127		eleq1 2848	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o} ↔ ∅ ∈ {1o, 2o}))
128	96, 127	mtbiri 330	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → ¬ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o})
129	126, 128	nsyli 158	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋)))
130	2, 129	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋)))
131	130	imp 412	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
132	131	adantrr 730	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
133	44	simplbi2 506	. . . . . . . . . . . . 13 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴 → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋)))
134	133	con3d 153	. . . . . . . . . . . 12 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 → (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴))
135	119, 132, 134	sylc 66	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴)
136	135	ex 418	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴))
137		ndmfv 6917	. . . . . . . . . 10 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴 → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
138	136, 137	syl6 36	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅))
139	115	adantl 487	. . . . . . . . . 10 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)
140	139	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o))
141	138, 140	jcad 522	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
142	109, 117, 141	3orim123d 1472	. . . . . . 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 6898	. . . . . . . 8 ⊢ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
144		fvex 6898	. . . . . . . 8 ⊢ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
145	143, 144	brtp 5496	. . . . . . 7 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
146	142, 15, 145	3imtr4g 299	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
147	12, 146	sylbid 243	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
148	147	imp 412	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
149		raleq 3316	. . . . . 6 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ↔ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)))
150		fveq2 6885	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (𝐴‘𝑥) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
151		fveq2 6885	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (𝐵‘𝑥) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
152	150, 151	breq12d 5115	. . . . . 6 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
153	149, 152	anbi12d 644	. . . . 5 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))))
154	153	rspcev 3576	. . . 4 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
155	9, 78, 148, 154	syl12anc 850	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
156		ltsval 28009	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
157	156	3adant3 1150	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
158	157	adantr 486	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
159	155, 158	mpbird 260	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → 𝐴 <s 𝐵)
160	159	ex 418	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → 𝐴 <s 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ⊆ wss 3895  ∅c0 4278  {cpr 4586  {ctp 4588  ⟨cop 4834  ∩ cint 4906   class class class wbr 5102  dom cdm 5650  ran crn 5651   ↾ cres 5652  Oncon0 6362  Fun wfun 6532  ‘cfv 6538  1_oc1o 8472  2_oc2o 8473  Nocsur 28002   <s clts 28003

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-br 5103  df-opab 5167  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ord 6365  df-on 6366  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-1o 8479  df-2o 8480  df-no 28005  df-lts 28006

This theorem is used by:  noresle  28059  nosupbnd1lem1  28070  nosupbnd1lem2  28071  nosupbnd1  28076  nosupbnd2lem1  28077  nosupbnd2  28078  noinfbnd1lem1  28085  noinfbnd1lem2  28086  noinfbnd1  28091  noinfbnd2lem1  28092  noinfbnd2  28093  noetasuplem3  28097  noetasuplem4  28098  noetainflem3  28101  noetainflem4  28102