Theorem sltres 33792

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 33790	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑋 ∈ On) → (𝐴 ↾ 𝑋) ∈ No )
2	1	3adant2 1129	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐴 ↾ 𝑋) ∈ No )
3		noreson 33790	. . . . . . 7 ⊢ ((𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐵 ↾ 𝑋) ∈ No )
4	3	3adant1 1128	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐵 ↾ 𝑋) ∈ No )
5		sltintdifex 33791	. . . . . . 7 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No ) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ V))
6		onintrab 7623	. . . . . . 7 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ V ↔ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On)
7	5, 6	syl6ib 250	. . . . . 6 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No ) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On))
8	2, 4, 7	syl2anc 583	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On))
9	8	imp 406	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On)
10		simpl3 1191	. . . . . . . 8 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → 𝑋 ∈ On)
11		sltval2 33786	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No ) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) ↔ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
12	2, 4, 11	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) ↔ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
13		fvex 6769	. . . . . . . . . . . . 13 ⊢ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
14		fvex 6769	. . . . . . . . . . . . 13 ⊢ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
15	13, 14	brtp 33623	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
16		1n0 8286	. . . . . . . . . . . . . . . . . 18 ⊢ 1o ≠ ∅
17	16	neii 2944	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1o = ∅
18		eqeq1 2742	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ 1o = ∅))
19	17, 18	mtbiri 326	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ¬ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
20		ndmfv 6786	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
21	19, 20	nsyl2 141	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
22	21	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
23	22	orcd 869	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
24	21	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
25	24	orcd 869	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
26		2on 8275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2o ∈ On
27	26	elexi 3441	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2o ∈ V
28	27	prid2 4696	. . . . . . . . . . . . . . . . . . 19 ⊢ 2o ∈ {1o, 2o}
29	28	nosgnn0i 33789	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ≠ 2o
30	29	neii 2944	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ∅ = 2o
31		eqeq1 2742	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ 2o = ∅))
32		eqcom 2745	. . . . . . . . . . . . . . . . . 18 ⊢ (2o = ∅ ↔ ∅ = 2o)
33	31, 32	bitrdi 286	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ ∅ = 2o))
34	30, 33	mtbiri 326	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ¬ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
35		ndmfv 6786	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
36	34, 35	nsyl2 141	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
37	36	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
38	37	olcd 870	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
39	23, 25, 38	3jaoi 1425	. . . . . . . . . . . 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	syl6bi 252	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))))
42	41	imp 406	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
43		dmres 5902	. . . . . . . . . . . 12 ⊢ dom (𝐴 ↾ 𝑋) = (𝑋 ∩ dom 𝐴)
44	43	elin2 4127	. . . . . . . . . . 11 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ↔ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴))
45	44	simplbi 497	. . . . . . . . . 10 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
46		dmres 5902	. . . . . . . . . . . 12 ⊢ dom (𝐵 ↾ 𝑋) = (𝑋 ∩ dom 𝐵)
47	46	elin2 4127	. . . . . . . . . . 11 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) ↔ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵))
48	47	simplbi 497	. . . . . . . . . 10 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
49	45, 48	jaoi 853	. . . . . . . . 9 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
50	42, 49	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
51		onelss 6293	. . . . . . . 8 ⊢ (𝑋 ∈ On → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑋))
52	10, 50, 51	sylc 65	. . . . . . 7 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑋)
53	52	sselda 3917	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ 𝑋)
54		onelon 6276	. . . . . . . . 9 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ On)
55	9, 54	sylan 579	. . . . . . . 8 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ On)
56		intss1 4891	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑦)
57		ontri1 6285	. . . . . . . . . . . . 13 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑦 ↔ ¬ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
58	56, 57	syl5ib 243	. . . . . . . . . . . 12 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
59	58	con2d 134	. . . . . . . . . . 11 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
60	9, 59	sylan 579	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ On) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
61	60	impancom 451	. . . . . . . . 9 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (𝑦 ∈ On → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
62	55, 61	mpd 15	. . . . . . . 8 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})
63		fveq2 6756	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑦 → ((𝐴 ↾ 𝑋)‘𝑎) = ((𝐴 ↾ 𝑋)‘𝑦))
64		fveq2 6756	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑦 → ((𝐵 ↾ 𝑋)‘𝑎) = ((𝐵 ↾ 𝑋)‘𝑦))
65	63, 64	neeq12d 3004	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑦 → (((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎) ↔ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦)))
66	65	elrab 3617	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ↔ (𝑦 ∈ On ∧ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦)))
67	66	simplbi2 500	. . . . . . . . 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 2943	. . . . . . . 8 ⊢ (((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦))
71	70	con2bii 357	. . . . . . 7 ⊢ (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦))
72	69, 71	sylibr 233	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦))
73		fvres 6775	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑋 → ((𝐴 ↾ 𝑋)‘𝑦) = (𝐴‘𝑦))
74		fvres 6775	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑋 → ((𝐵 ↾ 𝑋)‘𝑦) = (𝐵‘𝑦))
75	73, 74	eqeq12d 2754	. . . . . . 7 ⊢ (𝑦 ∈ 𝑋 → (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) ↔ (𝐴‘𝑦) = (𝐵‘𝑦)))
76	75	biimpd 228	. . . . . 6 ⊢ (𝑦 ∈ 𝑋 → (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) → (𝐴‘𝑦) = (𝐵‘𝑦)))
77	53, 72, 76	sylc 65	. . . . 5 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (𝐴‘𝑦) = (𝐵‘𝑦))
78	77	ralrimiva 3107	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦))
79		fvresval 33647	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∨ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
80	79	ori 857	. . . . . . . . . . . . . 14 ⊢ (¬ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
81	19, 80	nsyl2 141	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
82	81	eqcomd 2744	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
83		eqeq2 2750	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o))
84	82, 83	mpbid 231	. . . . . . . . . . 11 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o)
85	84	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o)
86	85	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o))
87	21	ad2antrl 724	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
88	87, 45	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
89		nofun 33779	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ↾ 𝑋) ∈ No → Fun (𝐵 ↾ 𝑋))
90		fvelrn 6936	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun (𝐵 ↾ 𝑋) ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋))
91	90	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun (𝐵 ↾ 𝑋) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋)))
92	89, 91	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋)))
93		norn 33781	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ↾ 𝑋) ∈ No → ran (𝐵 ↾ 𝑋) ⊆ {1o, 2o})
94	93	sseld 3916	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
95	92, 94	syld 47	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
96		nosgnn0 33788	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ∅ ∈ {1o, 2o}
97		eleq1 2826	. . . . . . . . . . . . . . . . 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 406	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
102	101	adantrl 712	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
103	47	simplbi2 500	. . . . . . . . . . . . 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 6786	. . . . . . . . . . 11 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵 → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
107	105, 106	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
108	107	ex 412	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅))
109	86, 108	jcad 512	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)))
110		fvresval 33647	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∨ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
111	110	ori 857	. . . . . . . . . . . . 13 ⊢ (¬ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
112	34, 111	nsyl2 141	. . . . . . . . . . . 12 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
113	112	eqcomd 2744	. . . . . . . . . . 11 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
114		eqeq2 2750	. . . . . . . . . . 11 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ((𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o))
115	113, 114	mpbid 231	. . . . . . . . . 10 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)
116	84, 115	anim12i 612	. . . . . . . . 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 725	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
119	118, 48	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
120		nofun 33779	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ↾ 𝑋) ∈ No → Fun (𝐴 ↾ 𝑋))
121		fvelrn 6936	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun (𝐴 ↾ 𝑋) ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋)) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋))
122	121	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun (𝐴 ↾ 𝑋) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋)))
123	120, 122	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋)))
124		norn 33781	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ↾ 𝑋) ∈ No → ran (𝐴 ↾ 𝑋) ⊆ {1o, 2o})
125	124	sseld 3916	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
126	123, 125	syld 47	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
127		eleq1 2826	. . . . . . . . . . . . . . . . 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 406	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
132	131	adantrr 713	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
133	44	simplbi2 500	. . . . . . . . . . . . 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 412	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴))
137		ndmfv 6786	. . . . . . . . . 10 ⊢ (¬ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴 → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
138	136, 137	syl6 35	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅))
139	115	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)
140	139	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o))
141	138, 140	jcad 512	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
142	109, 117, 141	3orim123d 1442	. . . . . . 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 6769	. . . . . . . 8 ⊢ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
144		fvex 6769	. . . . . . . 8 ⊢ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
145	143, 144	brtp 33623	. . . . . . 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 406	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
149		raleq 3333	. . . . . 6 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ↔ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)))
150		fveq2 6756	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (𝐴‘𝑥) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
151		fveq2 6756	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (𝐵‘𝑥) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
152	150, 151	breq12d 5083	. . . . . 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 3552	. . . 4 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
155	9, 78, 148, 154	syl12anc 833	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
156		sltval 33777	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
157	156	3adant3 1130	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
158	157	adantr 480	. . 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 412	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → 𝐴 <s 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   ∨ w3o 1084   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  {crab 3067  Vcvv 3422   ⊆ wss 3883  ∅c0 4253  {cpr 4560  {ctp 4562  ⟨cop 4564  ∩ cint 4876   class class class wbr 5070  dom cdm 5580  ran crn 5581   ↾ cres 5582  Oncon0 6251  Fun wfun 6412  ‘cfv 6418  1_oc1o 8260  2_oc2o 8261   No csur 33770   <s cslt 33771

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-ord 6254  df-on 6255  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-1o 8267  df-2o 8268  df-no 33773  df-slt 33774

This theorem is referenced by:  noresle  33827  nosupbnd1lem1  33838  nosupbnd1lem2  33839  nosupbnd1  33844  nosupbnd2lem1  33845  nosupbnd2  33846  noinfbnd1lem1  33853  noinfbnd1lem2  33854  noinfbnd1  33859  noinfbnd2lem1  33860  noinfbnd2  33861  noetasuplem3  33865  noetasuplem4  33866  noetainflem3  33869  noetainflem4  33870