Theorem sltres 27613

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.

Step	Hyp	Ref	Expression
1		noreson 27611	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑋 ∈ On) → (𝐴 ↾ 𝑋) ∈ No )
2	1	3adant2 1128	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐴 ↾ 𝑋) ∈ No )
3		noreson 27611	. . . . . . 7 ⊢ ((𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐵 ↾ 𝑋) ∈ No )
4	3	3adant1 1127	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐵 ↾ 𝑋) ∈ No )
5		sltintdifex 27612	. . . . . . 7 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No ) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ V))
6		onintrab 7803	. . . . . . 7 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ V ↔ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On)
7	5, 6	imbitrdi 250	. . . . . 6 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No ) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On))
8	2, 4, 7	syl2anc 582	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On))
9	8	imp 405	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On)
10		simpl3 1190	. . . . . . . 8 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → 𝑋 ∈ On)
11		sltval2 27607	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No ) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) ↔ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
12	2, 4, 11	syl2anc 582	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) ↔ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
13		fvex 6913	. . . . . . . . . . . . 13 ⊢ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
14		fvex 6913	. . . . . . . . . . . . 13 ⊢ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
15	13, 14	brtp 5527	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
16		1n0 8513	. . . . . . . . . . . . . . . . . 18 ⊢ 1o ≠ ∅
17	16	neii 2938	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1o = ∅
18		eqeq1 2731	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ 1o = ∅))
19	17, 18	mtbiri 326	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ¬ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
20		ndmfv 6935	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
21	19, 20	nsyl2 141	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
22	21	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
23	22	orcd 871	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
24	21	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
25	24	orcd 871	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
26		2on 8505	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2o ∈ On
27	26	elexi 3491	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2o ∈ V
28	27	prid2 4770	. . . . . . . . . . . . . . . . . . 19 ⊢ 2o ∈ {1o, 2o}
29	28	nosgnn0i 27610	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ≠ 2o
30	29	neii 2938	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ∅ = 2o
31		eqeq1 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ 2o = ∅))
32		eqcom 2734	. . . . . . . . . . . . . . . . . 18 ⊢ (2o = ∅ ↔ ∅ = 2o)
33	31, 32	bitrdi 286	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ ∅ = 2o))
34	30, 33	mtbiri 326	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ¬ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
35		ndmfv 6935	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
36	34, 35	nsyl2 141	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
37	36	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
38	37	olcd 872	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
39	23, 25, 38	3jaoi 1424	. . . . . . . . . . . 12 ⊢ (((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
40	15, 39	sylbi 216	. . . . . . . . . . 11 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
41	12, 40	biimtrdi 252	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))))
42	41	imp 405	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
43		dmres 6019	. . . . . . . . . . . 12 ⊢ dom (𝐴 ↾ 𝑋) = (𝑋 ∩ dom 𝐴)
44	43	elin2 4197	. . . . . . . . . . 11 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ↔ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴))
45	44	simplbi 496	. . . . . . . . . 10 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
46		dmres 6019	. . . . . . . . . . . 12 ⊢ dom (𝐵 ↾ 𝑋) = (𝑋 ∩ dom 𝐵)
47	46	elin2 4197	. . . . . . . . . . 11 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) ↔ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵))
48	47	simplbi 496	. . . . . . . . . 10 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
49	45, 48	jaoi 855	. . . . . . . . 9 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
50	42, 49	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
51		onelss 6414	. . . . . . . 8 ⊢ (𝑋 ∈ On → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑋))
52	10, 50, 51	sylc 65	. . . . . . 7 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑋)
53	52	sselda 3980	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ 𝑋)
54		onelon 6397	. . . . . . . . 9 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ On)
55	9, 54	sylan 578	. . . . . . . 8 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ On)
56		intss1 4968	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑦)
57		ontri1 6406	. . . . . . . . . . . . 13 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑦 ↔ ¬ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
58	56, 57	imbitrid 243	. . . . . . . . . . . 12 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
59	58	con2d 134	. . . . . . . . . . 11 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
60	9, 59	sylan 578	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ On) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
61	60	impancom 450	. . . . . . . . 9 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (𝑦 ∈ On → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
62	55, 61	mpd 15	. . . . . . . 8 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})
63		fveq2 6900	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑦 → ((𝐴 ↾ 𝑋)‘𝑎) = ((𝐴 ↾ 𝑋)‘𝑦))
64		fveq2 6900	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑦 → ((𝐵 ↾ 𝑋)‘𝑎) = ((𝐵 ↾ 𝑋)‘𝑦))
65	63, 64	neeq12d 2998	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑦 → (((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎) ↔ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦)))
66	65	elrab 3682	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ↔ (𝑦 ∈ On ∧ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦)))
67	66	simplbi2 499	. . . . . . . . 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 2937	. . . . . . . 8 ⊢ (((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦))
71	70	con2bii 356	. . . . . . 7 ⊢ (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦))
72	69, 71	sylibr 233	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦))
73		fvres 6919	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑋 → ((𝐴 ↾ 𝑋)‘𝑦) = (𝐴‘𝑦))
74		fvres 6919	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑋 → ((𝐵 ↾ 𝑋)‘𝑦) = (𝐵‘𝑦))
75	73, 74	eqeq12d 2743	. . . . . . 7 ⊢ (𝑦 ∈ 𝑋 → (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) ↔ (𝐴‘𝑦) = (𝐵‘𝑦)))
76	75	biimpd 228	. . . . . 6 ⊢ (𝑦 ∈ 𝑋 → (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) → (𝐴‘𝑦) = (𝐵‘𝑦)))
77	53, 72, 76	sylc 65	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (𝐴‘𝑦) = (𝐵‘𝑦))
78	77	ralrimiva 3142	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦))
79		fvresval 7370	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∨ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
80	79	ori 859	. . . . . . . . . . . . . 14 ⊢ (¬ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
81	19, 80	nsyl2 141	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
82	81	eqcomd 2733	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
83		eqeq2 2739	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o))
84	82, 83	mpbid 231	. . . . . . . . . . 11 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o)
85	84	adantr 479	. . . . . . . . . 10 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o)
86	85	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o))
87	21	ad2antrl 726	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
88	87, 45	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
89		nofun 27600	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ↾ 𝑋) ∈ No → Fun (𝐵 ↾ 𝑋))
90		fvelrn 7089	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun (𝐵 ↾ 𝑋) ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋))
91	90	ex 411	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun (𝐵 ↾ 𝑋) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋)))
92	89, 91	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋)))
93		norn 27602	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ↾ 𝑋) ∈ No → ran (𝐵 ↾ 𝑋) ⊆ {1o, 2o})
94	93	sseld 3979	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
95	92, 94	syld 47	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
96		nosgnn0 27609	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ∅ ∈ {1o, 2o}
97		eleq1 2816	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o} ↔ ∅ ∈ {1o, 2o}))
98	96, 97	mtbiri 326	. . . . . . . . . . . . . . . 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 405	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
102	101	adantrl 714	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
103	47	simplbi2 499	. . . . . . . . . . . . 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 6935	. . . . . . . . . . 11 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵 → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
107	105, 106	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
108	107	ex 411	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅))
109	86, 108	jcad 511	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)))
110		fvresval 7370	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∨ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
111	110	ori 859	. . . . . . . . . . . . 13 ⊢ (¬ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
112	34, 111	nsyl2 141	. . . . . . . . . . . 12 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
113	112	eqcomd 2733	. . . . . . . . . . 11 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
114		eqeq2 2739	. . . . . . . . . . 11 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ((𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o))
115	113, 114	mpbid 231	. . . . . . . . . 10 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)
116	84, 115	anim12i 611	. . . . . . . . 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 727	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
119	118, 48	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
120		nofun 27600	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ↾ 𝑋) ∈ No → Fun (𝐴 ↾ 𝑋))
121		fvelrn 7089	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun (𝐴 ↾ 𝑋) ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋)) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋))
122	121	ex 411	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun (𝐴 ↾ 𝑋) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋)))
123	120, 122	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋)))
124		norn 27602	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ↾ 𝑋) ∈ No → ran (𝐴 ↾ 𝑋) ⊆ {1o, 2o})
125	124	sseld 3979	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
126	123, 125	syld 47	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
127		eleq1 2816	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o} ↔ ∅ ∈ {1o, 2o}))
128	96, 127	mtbiri 326	. . . . . . . . . . . . . . . 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 405	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
132	131	adantrr 715	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
133	44	simplbi2 499	. . . . . . . . . . . . 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 411	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴))
137		ndmfv 6935	. . . . . . . . . 10 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴 → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
138	136, 137	syl6 35	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅))
139	115	adantl 480	. . . . . . . . . 10 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)
140	139	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o))
141	138, 140	jcad 511	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
142	109, 117, 141	3orim123d 1440	. . . . . . 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 6913	. . . . . . . 8 ⊢ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
144		fvex 6913	. . . . . . . 8 ⊢ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
145	143, 144	brtp 5527	. . . . . . 7 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
146	142, 15, 145	3imtr4g 295	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
147	12, 146	sylbid 239	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
148	147	imp 405	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
149		raleq 3318	. . . . . 6 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ↔ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)))
150		fveq2 6900	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (𝐴‘𝑥) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
151		fveq2 6900	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (𝐵‘𝑥) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
152	150, 151	breq12d 5163	. . . . . 6 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
153	149, 152	anbi12d 630	. . . . 5 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))))
154	153	rspcev 3609	. . . 4 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
155	9, 78, 148, 154	syl12anc 835	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
156		sltval 27598	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
157	156	3adant3 1129	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
158	157	adantr 479	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
159	155, 158	mpbird 256	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → 𝐴 <s 𝐵)
160	159	ex 411	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → 𝐴 <s 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∨ w3o 1083   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   ≠ wne 2936  ∀wral 3057  ∃wrex 3066  {crab 3428  Vcvv 3471   ⊆ wss 3947  ∅c0 4324  {cpr 4632  {ctp 4634  ⟨cop 4636  ∩ cint 4951   class class class wbr 5150  dom cdm 5680  ran crn 5681   ↾ cres 5682  Oncon0 6372  Fun wfun 6545  ‘cfv 6551  1_oc1o 8484  2_oc2o 8485   No csur 27591   <s cslt 27592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pr 5431

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-ral 3058  df-rex 3067  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4911  df-int 4952  df-iun 5000  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-ord 6375  df-on 6376  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-1o 8491  df-2o 8492  df-no 27594  df-slt 27595

This theorem is referenced by:  noresle  27648  nosupbnd1lem1  27659  nosupbnd1lem2  27660  nosupbnd1  27665  nosupbnd2lem1  27666  nosupbnd2  27667  noinfbnd1lem1  27674  noinfbnd1lem2  27675  noinfbnd1  27680  noinfbnd2lem1  27681  noinfbnd2  27682  noetasuplem3  27686  noetasuplem4  27687  noetainflem3  27690  noetainflem4  27691