Theorem sltres 27626

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 27624	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑋 ∈ On) → (𝐴 ↾ 𝑋) ∈ No )
2	1	3adant2 1131	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐴 ↾ 𝑋) ∈ No )
3		noreson 27624	. . . . . . 7 ⊢ ((𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐵 ↾ 𝑋) ∈ No )
4	3	3adant1 1130	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (𝐵 ↾ 𝑋) ∈ No )
5		sltintdifex 27625	. . . . . . 7 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No ) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ V))
6		onintrab 7790	. . . . . . 7 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ V ↔ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On)
7	5, 6	imbitrdi 251	. . . . . 6 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No ) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On))
8	2, 4, 7	syl2anc 584	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On))
9	8	imp 406	. . . 4 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On)
10		simpl3 1194	. . . . . . . 8 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → 𝑋 ∈ On)
11		sltval2 27620	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋) ∈ No ∧ (𝐵 ↾ 𝑋) ∈ No ) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) ↔ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
12	2, 4, 11	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) ↔ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
13		fvex 6889	. . . . . . . . . . . . 13 ⊢ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
14		fvex 6889	. . . . . . . . . . . . 13 ⊢ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
15	13, 14	brtp 5498	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
16		1n0 8500	. . . . . . . . . . . . . . . . . 18 ⊢ 1o ≠ ∅
17	16	neii 2934	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1o = ∅
18		eqeq1 2739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ 1o = ∅))
19	17, 18	mtbiri 327	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ¬ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
20		ndmfv 6911	. . . . . . . . . . . . . . . 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 873	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
24	21	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
25	24	orcd 873	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
26		2on 8494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2o ∈ On
27	26	elexi 3482	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2o ∈ V
28	27	prid2 4739	. . . . . . . . . . . . . . . . . . 19 ⊢ 2o ∈ {1o, 2o}
29	28	nosgnn0i 27623	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ≠ 2o
30	29	neii 2934	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ∅ = 2o
31		eqeq1 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ 2o = ∅))
32		eqcom 2742	. . . . . . . . . . . . . . . . . 18 ⊢ (2o = ∅ ↔ ∅ = 2o)
33	31, 32	bitrdi 287	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ↔ ∅ = 2o))
34	30, 33	mtbiri 327	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ¬ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
35		ndmfv 6911	. . . . . . . . . . . . . . . 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 874	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
39	23, 25, 38	3jaoi 1430	. . . . . . . . . . . 12 ⊢ (((((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) ∨ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
40	15, 39	sylbi 217	. . . . . . . . . . 11 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
41	12, 40	biimtrdi 253	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))))
42	41	imp 406	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)))
43		dmres 5999	. . . . . . . . . . . 12 ⊢ dom (𝐴 ↾ 𝑋) = (𝑋 ∩ dom 𝐴)
44	43	elin2 4178	. . . . . . . . . . 11 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ↔ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐴))
45	44	simplbi 497	. . . . . . . . . 10 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
46		dmres 5999	. . . . . . . . . . . 12 ⊢ dom (𝐵 ↾ 𝑋) = (𝑋 ∩ dom 𝐵)
47	46	elin2 4178	. . . . . . . . . . 11 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) ↔ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 ∧ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom 𝐵))
48	47	simplbi 497	. . . . . . . . . 10 ⊢ (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
49	45, 48	jaoi 857	. . . . . . . . 9 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) ∨ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
50	42, 49	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
51		onelss 6394	. . . . . . . 8 ⊢ (𝑋 ∈ On → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋 → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑋))
52	10, 50, 51	sylc 65	. . . . . . 7 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑋)
53	52	sselda 3958	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ 𝑋)
54		onelon 6377	. . . . . . . . 9 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ On)
55	9, 54	sylan 580	. . . . . . . 8 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → 𝑦 ∈ On)
56		intss1 4939	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑦)
57		ontri1 6386	. . . . . . . . . . . . 13 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ⊆ 𝑦 ↔ ¬ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
58	56, 57	imbitrid 244	. . . . . . . . . . . 12 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
59	58	con2d 134	. . . . . . . . . . 11 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ¬ 𝑦 ∈ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
60	9, 59	sylan 580	. . . . . . . . . 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 6876	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑦 → ((𝐴 ↾ 𝑋)‘𝑎) = ((𝐴 ↾ 𝑋)‘𝑦))
64		fveq2 6876	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑦 → ((𝐵 ↾ 𝑋)‘𝑎) = ((𝐵 ↾ 𝑋)‘𝑦))
65	63, 64	neeq12d 2993	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑦 → (((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎) ↔ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦)))
66	65	elrab 3671	. . . . . . . . . 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 2933	. . . . . . . 8 ⊢ (((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦))
71	70	con2bii 357	. . . . . . 7 ⊢ (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑦) ≠ ((𝐵 ↾ 𝑋)‘𝑦))
72	69, 71	sylibr 234	. . . . . 6 ⊢ ((((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦))
73		fvres 6895	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑋 → ((𝐴 ↾ 𝑋)‘𝑦) = (𝐴‘𝑦))
74		fvres 6895	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑋 → ((𝐵 ↾ 𝑋)‘𝑦) = (𝐵‘𝑦))
75	73, 74	eqeq12d 2751	. . . . . . 7 ⊢ (𝑦 ∈ 𝑋 → (((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦) ↔ (𝐴‘𝑦) = (𝐵‘𝑦)))
76	75	biimpd 229	. . . . . 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 7351	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∨ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
80	79	ori 861	. . . . . . . . . . . . . 14 ⊢ (¬ ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
81	19, 80	nsyl2 141	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
82	81	eqcomd 2741	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
83		eqeq2 2747	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o → ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o))
84	82, 83	mpbid 232	. . . . . . . . . . 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 728	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋))
88	87, 45	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
89		nofun 27613	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ↾ 𝑋) ∈ No → Fun (𝐵 ↾ 𝑋))
90		fvelrn 7066	. . . . . . . . . . . . . . . . . . 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 27615	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ↾ 𝑋) ∈ No → ran (𝐵 ↾ 𝑋) ⊆ {1o, 2o})
94	93	sseld 3957	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
95	92, 94	syld 47	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
96		nosgnn0 27622	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ∅ ∈ {1o, 2o}
97		eleq1 2822	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o} ↔ ∅ ∈ {1o, 2o}))
98	96, 97	mtbiri 327	. . . . . . . . . . . . . . . 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 716	. . . . . . . . . . . 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 6911	. . . . . . . . . . 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 7351	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∨ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
111	110	ori 861	. . . . . . . . . . . . 13 ⊢ (¬ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅)
112	34, 111	nsyl2 141	. . . . . . . . . . . 12 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
113	112	eqcomd 2741	. . . . . . . . . . 11 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
114		eqeq2 2747	. . . . . . . . . . 11 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → ((𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o))
115	113, 114	mpbid 232	. . . . . . . . . 10 ⊢ (((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o → (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)
116	84, 115	anim12i 613	. . . . . . . . 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 729	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐵 ↾ 𝑋))
119	118, 48	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)) → ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ 𝑋)
120		nofun 27613	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ↾ 𝑋) ∈ No → Fun (𝐴 ↾ 𝑋))
121		fvelrn 7066	. . . . . . . . . . . . . . . . . . 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 27615	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ↾ 𝑋) ∈ No → ran (𝐴 ↾ 𝑋) ⊆ {1o, 2o})
125	124	sseld 3957	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ ran (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
126	123, 125	syld 47	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ↾ 𝑋) ∈ No → (∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ dom (𝐴 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o}))
127		eleq1 2822	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ {1o, 2o} ↔ ∅ ∈ {1o, 2o}))
128	96, 127	mtbiri 327	. . . . . . . . . . . . . . . 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 717	. . . . . . . . . . . 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 6911	. . . . . . . . . 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 1446	. . . . . . 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 6889	. . . . . . . 8 ⊢ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
144		fvex 6889	. . . . . . . 8 ⊢ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ∈ V
145	143, 144	brtp 5498	. . . . . . 7 ⊢ ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) ↔ (((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) = 2o)))
146	142, 15, 145	3imtr4g 296	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → (((𝐴 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵 ↾ 𝑋)‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}) → (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
147	12, 146	sylbid 240	. . . . 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 3302	. . . . . 6 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ↔ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)))
150		fveq2 6876	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (𝐴‘𝑥) = (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
151		fveq2 6876	. . . . . . 7 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → (𝐵‘𝑥) = (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))
152	150, 151	breq12d 5132	. . . . . 6 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ((𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)})))
153	149, 152	anbi12d 632	. . . . 5 ⊢ (𝑥 = ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} → ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)) ↔ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))))
154	153	rspcev 3601	. . . 4 ⊢ ((∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ ((𝐴 ↾ 𝑋)‘𝑎) ≠ ((𝐵 ↾ 𝑋)‘𝑎)}))) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
155	9, 78, 148, 154	syl12anc 836	. . 3 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))
156		sltval 27611	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
157	156	3adant3 1132	. . . 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 257	. 2 ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ (𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋)) → 𝐴 <s 𝐵)
160	159	ex 412	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → 𝐴 <s 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∨ w3o 1085   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  {crab 3415  Vcvv 3459   ⊆ wss 3926  ∅c0 4308  {cpr 4603  {ctp 4605  ⟨cop 4607  ∩ cint 4922   class class class wbr 5119  dom cdm 5654  ran crn 5655   ↾ cres 5656  Oncon0 6352  Fun wfun 6525  ‘cfv 6531  1_oc1o 8473  2_oc2o 8474   No csur 27603   <s cslt 27604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-tp 4606  df-op 4608  df-uni 4884  df-int 4923  df-br 5120  df-opab 5182  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ord 6355  df-on 6356  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-1o 8480  df-2o 8481  df-no 27606  df-slt 27607

This theorem is referenced by:  noresle  27661  nosupbnd1lem1  27672  nosupbnd1lem2  27673  nosupbnd1  27678  nosupbnd2lem1  27679  nosupbnd2  27680  noinfbnd1lem1  27687  noinfbnd1lem2  27688  noinfbnd1  27693  noinfbnd2lem1  27694  noinfbnd2  27695  noetasuplem3  27699  noetasuplem4  27700  noetainflem3  27703  noetainflem4  27704