Theorem ltsres 27651

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 27649	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑋 ∈ On) → (𝐴 ↾ 𝑋) ∈ No )
2	1	3adant2 1137	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐴 ↾ 𝑋) ∈ No )
3		noreson 27649	. . . . . . 7 ⊢ ((𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐵 ↾ 𝑋) ∈ No )
4	3	3adant1 1136	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐵 ↾ 𝑋) ∈ No )
5		ltsintdifex 27650	. . . . . . 7 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No ) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ V))
6		onintrab 7746	. . . . . . 7 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ V ↔ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On)
7	5, 6	imbitrdi 252	. . . . . 6 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No ) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On))
8	2, 4, 7	syl2anc 590	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On))
9	8	imp 407	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On)
10		simpl3 1200	. . . . . . . 8 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → 𝑋 ∈ On)
11		ltsval2 27645	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No ) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) ↔ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
12	2, 4, 11	syl2anc 590	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) ↔ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
13		fvex 6847	. . . . . . . . . . . . 13 ⊢ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
14		fvex 6847	. . . . . . . . . . . . 13 ⊢ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
15	13, 14	brtp 5472	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
16		1n0 8420	. . . . . . . . . . . . . . . . . 18 ⊢ 1o ≠ ∅
17	16	neii 2937	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1o = ∅
18		eqeq1 2744	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ 1o = ∅))
19	17, 18	mtbiri 328	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ¬ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
20		ndmfv 6866	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
21	19, 20	nsyl2 141	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
22	21	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
23	22	orcd 879	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
24	21	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
25	24	orcd 879	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
26		2on 8415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2o ∈ On
27	26	elexi 3455	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2o ∈ V
28	27	prid2 4702	. . . . . . . . . . . . . . . . . . 19 ⊢ 2o ∈ {1o, 2o}
29	28	nosgnn0i 27648	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ≠ 2o
30	29	neii 2937	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ∅ = 2o
31		eqeq1 2744	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ 2o = ∅))
32		eqcom 2747	. . . . . . . . . . . . . . . . . 18 ⊢ (2o = ∅ ↔ ∅ = 2o)
33	31, 32	bitrdi 288	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ ∅ = 2o))
34	30, 33	mtbiri 328	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ¬ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
35		ndmfv 6866	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
36	34, 35	nsyl2 141	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
37	36	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
38	37	olcd 880	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
39	23, 25, 38	3jaoi 1436	. . . . . . . . . . . 12 ⊢ (((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
40	15, 39	sylbi 218	. . . . . . . . . . 11 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
41	12, 40	biimtrdi 254	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))))
42	41	imp 407	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
43		dmres 5971	. . . . . . . . . . . 12 ⊢ dom (𝐴 ↾ 𝑋) = (𝑋 ∩ dom 𝐴)
44	43	elin2 4139	. . . . . . . . . . 11 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ↔ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴))
45	44	simplbi 497	. . . . . . . . . 10 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
46		dmres 5971	. . . . . . . . . . . 12 ⊢ dom (𝐵 ↾ 𝑋) = (𝑋 ∩ dom 𝐵)
47	46	elin2 4139	. . . . . . . . . . 11 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) ↔ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵))
48	47	simplbi 497	. . . . . . . . . 10 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
49	45, 48	jaoi 863	. . . . . . . . 9 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
50	42, 49	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
51		onelss 6359	. . . . . . . 8 ⊢ (𝑋 ∈ On → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑋))
52	10, 50, 51	sylc 65	. . . . . . 7 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑋)
53	52	sselda 3922	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ 𝑋)
54		onelon 6342	. . . . . . . . 9 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ On)
55	9, 54	sylan 586	. . . . . . . 8 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ On)
56		intss1 4900	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑦)
57		ontri1 6351	. . . . . . . . . . . . 13 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑦 ↔ ¬ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
58	56, 57	imbitrid 245	. . . . . . . . . . . 12 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
59	58	con2d 134	. . . . . . . . . . 11 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
60	9, 59	sylan 586	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ On) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
61	60	impancom 452	. . . . . . . . 9 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (𝑦 ∈ On → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
62	55, 61	mpd 15	. . . . . . . 8 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})
63		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑦 → ((𝐴 ↾ 𝑋)‘𝑎) = ((𝐴 ↾ 𝑋)‘𝑦))
64		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑦 → ((𝐵 ↾ 𝑋)‘𝑎) = ((𝐵 ↾ 𝑋)‘𝑦))
65	63, 64	neeq12d 2996	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑦 → (((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎) ↔ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦)))
66	65	elrab 3636	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ↔ (𝑦 ∈ On ∧ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦)))
67	66	simplbi2 501	. . . . . . . . 9 ⊢ (𝑦 ∈ On → (((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦) → 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
68	67	con3d 152	. . . . . . . 8 ⊢ (𝑦 ∈ On → (¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦)))
69	55, 62, 68	sylc 65	. . . . . . 7 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ¬ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦))
70		df-ne 2936	. . . . . . . 8 ⊢ (((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦))
71	70	con2bii 358	. . . . . . 7 ⊢ (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦))
72	69, 71	sylibr 235	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦))
73		fvres 6853	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑋 → ((𝐴 ↾ 𝑋)‘𝑦) = (𝐴‘𝑦))
74		fvres 6853	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑋 → ((𝐵 ↾ 𝑋)‘𝑦) = (𝐵‘𝑦))
75	73, 74	eqeq12d 2756	. . . . . . 7 ⊢ (𝑦 ∈ 𝑋 → (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) ↔ (𝐴‘𝑦) = (𝐵‘𝑦)))
76	75	biimpd 230	. . . . . 6 ⊢ (𝑦 ∈ 𝑋 → (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) → (𝐴‘𝑦) = (𝐵‘𝑦)))
77	53, 72, 76	sylc 65	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (𝐴‘𝑦) = (𝐵‘𝑦))
78	77	ralrimiva 3132	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦))
79		fvresval 7309	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∨ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
80	79	ori 867	. . . . . . . . . . . . . 14 ⊢ (¬ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
81	19, 80	nsyl2 141	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
82	81	eqcomd 2746	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
83		eqeq2 2752	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o))
84	82, 83	mpbid 233	. . . . . . . . . . 11 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o)
85	84	adantr 481	. . . . . . . . . 10 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o)
86	85	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o))
87	21	ad2antrl 734	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
88	87, 45	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
89		nofun 27638	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ↾ 𝑋) ∈ No → Fun (𝐵 ↾ 𝑋))
90		fvelrn 7024	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun (𝐵 ↾ 𝑋) ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋))
91	90	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun (𝐵 ↾ 𝑋) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋)))
92	89, 91	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋)))
93		norn 27640	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ↾ 𝑋) ∈ No → ran (𝐵 ↾ 𝑋) ⊆ {1o, 2o})
94	93	sseld 3921	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
95	92, 94	syld 47	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
96		nosgnn0 27647	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ∅ ∈ {1o, 2o}
97		eleq1 2828	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o} ↔ ∅ ∈ {1o, 2o}))
98	96, 97	mtbiri 328	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → ¬ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o})
99	95, 98	nsyli 157	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
100	4, 99	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
101	100	imp 407	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
102	101	adantrl 722	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
103	47	simplbi2 501	. . . . . . . . . . . . 13 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵 → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
104	103	con3d 152	. . . . . . . . . . . 12 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 → (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵))
105	88, 102, 104	sylc 65	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵)
106		ndmfv 6866	. . . . . . . . . . 11 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵 → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
107	105, 106	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
108	107	ex 413	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅))
109	86, 108	jcad 517	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)))
110		fvresval 7309	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∨ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
111	110	ori 867	. . . . . . . . . . . . 13 ⊢ (¬ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
112	34, 111	nsyl2 141	. . . . . . . . . . . 12 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
113	112	eqcomd 2746	. . . . . . . . . . 11 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
114		eqeq2 2752	. . . . . . . . . . 11 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ((𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o))
115	113, 114	mpbid 233	. . . . . . . . . 10 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)
116	84, 115	anim12i 619	. . . . . . . . 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 735	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
119	118, 48	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
120		nofun 27638	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ↾ 𝑋) ∈ No → Fun (𝐴 ↾ 𝑋))
121		fvelrn 7024	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun (𝐴 ↾ 𝑋) ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋)) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋))
122	121	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun (𝐴 ↾ 𝑋) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋)))
123	120, 122	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋)))
124		norn 27640	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ↾ 𝑋) ∈ No → ran (𝐴 ↾ 𝑋) ⊆ {1o, 2o})
125	124	sseld 3921	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
126	123, 125	syld 47	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
127		eleq1 2828	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o} ↔ ∅ ∈ {1o, 2o}))
128	96, 127	mtbiri 328	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → ¬ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o})
129	126, 128	nsyli 157	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋)))
130	2, 129	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋)))
131	130	imp 407	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
132	131	adantrr 723	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
133	44	simplbi2 501	. . . . . . . . . . . . 13 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴 → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋)))
134	133	con3d 152	. . . . . . . . . . . 12 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 → (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴))
135	119, 132, 134	sylc 65	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴)
136	135	ex 413	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴))
137		ndmfv 6866	. . . . . . . . . 10 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴 → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
138	136, 137	syl6 35	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅))
139	115	adantl 482	. . . . . . . . . 10 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)
140	139	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o))
141	138, 140	jcad 517	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
142	109, 117, 141	3orim123d 1452	. . . . . . 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 6847	. . . . . . . 8 ⊢ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
144		fvex 6847	. . . . . . . 8 ⊢ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
145	143, 144	brtp 5472	. . . . . . 7 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
146	142, 15, 145	3imtr4g 297	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
147	12, 146	sylbid 241	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
148	147	imp 407	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
149		raleq 3295	. . . . . 6 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ↔ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)))
150		fveq2 6834	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (𝐴‘𝑥) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
151		fveq2 6834	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (𝐵‘𝑥) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
152	150, 151	breq12d 5092	. . . . . 6 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
153	149, 152	anbi12d 638	. . . . 5 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))))
154	153	rspcev 3567	. . . 4 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
155	9, 78, 148, 154	syl12anc 842	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
156		ltsval 27636	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
157	156	3adant3 1138	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
158	157	adantr 481	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
159	155, 158	mpbird 258	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → 𝐴 <s 𝐵)
160	159	ex 413	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → 𝐴 <s 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   ∨ w3o 1091   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   ≠ wne 2935  ∀wral 3054  ∃wrex 3064  {crab 3392  Vcvv 3432   ⊆ wss 3890  ∅c0 4268  {cpr 4564  {ctp 4566  ⟨cop 4568  ∩ cint 4884   class class class wbr 5079  dom cdm 5625  ran crn 5626   ↾ cres 5627  Oncon0 6317  Fun wfun 6486  ‘cfv 6492  1_oc1o 8395  2_oc2o 8396   No csur 27628   <s clts 27629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4846  df-int 4885  df-br 5080  df-opab 5142  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ord 6320  df-on 6321  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-1o 8402  df-2o 8403  df-no 27631  df-lts 27632

This theorem is referenced by:  noresle  27686  nosupbnd1lem1  27697  nosupbnd1lem2  27698  nosupbnd1  27703  nosupbnd2lem1  27704  nosupbnd2  27705  noinfbnd1lem1  27712  noinfbnd1lem2  27713  noinfbnd1  27718  noinfbnd2lem1  27719  noinfbnd2  27720  noetasuplem3  27724  noetasuplem4  27725  noetainflem3  27728  noetainflem4  27729