Metamath Proof Explorer


Theorem sltval2

Description: Alternate expression for surreal less than. Two surreals obey surreal less than iff they obey the sign ordering at the first place they differ. (Contributed by Scott Fenton, 17-Jun-2011)

Ref Expression
Assertion sltval2 ( ( 𝐴 No 𝐵 No ) → ( 𝐴 <s 𝐵 ↔ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )

Proof

Step Hyp Ref Expression
1 sltval ( ( 𝐴 No 𝐵 No ) → ( 𝐴 <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) ) )
2 fvex ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ∈ V
3 fvex ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ∈ V
4 2 3 brtp ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ↔ ( ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ ) ∨ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) ∨ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) ) )
5 1n0 1o ≠ ∅
6 5 neii ¬ 1o = ∅
7 eqeq1 ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ ↔ 1o = ∅ ) )
8 6 7 mtbiri ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o → ¬ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ )
9 fvprc ( ¬ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ V → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ )
10 8 9 nsyl2 ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ V )
11 10 adantr ( ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ V )
12 10 adantr ( ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ V )
13 2on0 2o ≠ ∅
14 13 neii ¬ 2o = ∅
15 eqeq1 ( ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o → ( ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ ↔ 2o = ∅ ) )
16 14 15 mtbiri ( ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o → ¬ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ )
17 fvprc ( ¬ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ V → ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ )
18 16 17 nsyl2 ( ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ V )
19 18 adantl ( ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ V )
20 11 12 19 3jaoi ( ( ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ ) ∨ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) ∨ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ V )
21 4 20 sylbi ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ V )
22 onintrab ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ V ↔ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On )
23 21 22 sylib ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On )
24 23 adantl ( ( ( 𝐴 No 𝐵 No ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On )
25 onelon ( ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On ∧ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → 𝑦 ∈ On )
26 25 expcom ( 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On → 𝑦 ∈ On ) )
27 24 26 syl5 ( 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ( ( 𝐴 No 𝐵 No ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) → 𝑦 ∈ On ) )
28 fveq2 ( 𝑎 = 𝑦 → ( 𝐴𝑎 ) = ( 𝐴𝑦 ) )
29 fveq2 ( 𝑎 = 𝑦 → ( 𝐵𝑎 ) = ( 𝐵𝑦 ) )
30 28 29 neeq12d ( 𝑎 = 𝑦 → ( ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) ↔ ( 𝐴𝑦 ) ≠ ( 𝐵𝑦 ) ) )
31 30 onnminsb ( 𝑦 ∈ On → ( 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ¬ ( 𝐴𝑦 ) ≠ ( 𝐵𝑦 ) ) )
32 31 com12 ( 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( 𝑦 ∈ On → ¬ ( 𝐴𝑦 ) ≠ ( 𝐵𝑦 ) ) )
33 27 32 syldc ( ( ( 𝐴 No 𝐵 No ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) → ( 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ¬ ( 𝐴𝑦 ) ≠ ( 𝐵𝑦 ) ) )
34 df-ne ( ( 𝐴𝑦 ) ≠ ( 𝐵𝑦 ) ↔ ¬ ( 𝐴𝑦 ) = ( 𝐵𝑦 ) )
35 34 con2bii ( ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ↔ ¬ ( 𝐴𝑦 ) ≠ ( 𝐵𝑦 ) )
36 33 35 syl6ibr ( ( ( 𝐴 No 𝐵 No ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) → ( 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) )
37 36 ralrimiv ( ( ( 𝐴 No 𝐵 No ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) → ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( 𝐵𝑦 ) )
38 24 37 jca ( ( ( 𝐴 No 𝐵 No ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) → ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On ∧ ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) )
39 38 ex ( ( 𝐴 No 𝐵 No ) → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On ∧ ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ) )
40 39 impac ( ( ( 𝐴 No 𝐵 No ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) → ( ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On ∧ ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
41 anass ( ( ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On ∧ ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ↔ ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On ∧ ( ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ) )
42 40 41 sylib ( ( ( 𝐴 No 𝐵 No ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) → ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On ∧ ( ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ) )
43 raleq ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ↔ ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) )
44 fveq2 ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( 𝐴𝑥 ) = ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
45 fveq2 ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( 𝐵𝑥 ) = ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
46 44 45 breq12d ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ↔ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
47 43 46 anbi12d ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) ↔ ( ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ) )
48 47 rspcev ( ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On ∧ ( ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) )
49 42 48 syl ( ( ( 𝐴 No 𝐵 No ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) )
50 49 ex ( ( 𝐴 No 𝐵 No ) → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) ) )
51 eqeq12 ( ( ( 𝐴𝑥 ) = 1o ∧ ( 𝐵𝑥 ) = ∅ ) → ( ( 𝐴𝑥 ) = ( 𝐵𝑥 ) ↔ 1o = ∅ ) )
52 6 51 mtbiri ( ( ( 𝐴𝑥 ) = 1o ∧ ( 𝐵𝑥 ) = ∅ ) → ¬ ( 𝐴𝑥 ) = ( 𝐵𝑥 ) )
53 1on 1o ∈ On
54 0elon ∅ ∈ On
55 suc11 ( ( 1o ∈ On ∧ ∅ ∈ On ) → ( suc 1o = suc ∅ ↔ 1o = ∅ ) )
56 55 necon3bid ( ( 1o ∈ On ∧ ∅ ∈ On ) → ( suc 1o ≠ suc ∅ ↔ 1o ≠ ∅ ) )
57 53 54 56 mp2an ( suc 1o ≠ suc ∅ ↔ 1o ≠ ∅ )
58 5 57 mpbir suc 1o ≠ suc ∅
59 df-2o 2o = suc 1o
60 df-1o 1o = suc ∅
61 59 60 eqeq12i ( 2o = 1o ↔ suc 1o = suc ∅ )
62 58 61 nemtbir ¬ 2o = 1o
63 eqeq12 ( ( ( 𝐴𝑥 ) = 1o ∧ ( 𝐵𝑥 ) = 2o ) → ( ( 𝐴𝑥 ) = ( 𝐵𝑥 ) ↔ 1o = 2o ) )
64 eqcom ( 1o = 2o ↔ 2o = 1o )
65 63 64 bitrdi ( ( ( 𝐴𝑥 ) = 1o ∧ ( 𝐵𝑥 ) = 2o ) → ( ( 𝐴𝑥 ) = ( 𝐵𝑥 ) ↔ 2o = 1o ) )
66 62 65 mtbiri ( ( ( 𝐴𝑥 ) = 1o ∧ ( 𝐵𝑥 ) = 2o ) → ¬ ( 𝐴𝑥 ) = ( 𝐵𝑥 ) )
67 13 nesymi ¬ ∅ = 2o
68 eqeq12 ( ( ( 𝐴𝑥 ) = ∅ ∧ ( 𝐵𝑥 ) = 2o ) → ( ( 𝐴𝑥 ) = ( 𝐵𝑥 ) ↔ ∅ = 2o ) )
69 67 68 mtbiri ( ( ( 𝐴𝑥 ) = ∅ ∧ ( 𝐵𝑥 ) = 2o ) → ¬ ( 𝐴𝑥 ) = ( 𝐵𝑥 ) )
70 52 66 69 3jaoi ( ( ( ( 𝐴𝑥 ) = 1o ∧ ( 𝐵𝑥 ) = ∅ ) ∨ ( ( 𝐴𝑥 ) = 1o ∧ ( 𝐵𝑥 ) = 2o ) ∨ ( ( 𝐴𝑥 ) = ∅ ∧ ( 𝐵𝑥 ) = 2o ) ) → ¬ ( 𝐴𝑥 ) = ( 𝐵𝑥 ) )
71 fvex ( 𝐴𝑥 ) ∈ V
72 fvex ( 𝐵𝑥 ) ∈ V
73 71 72 brtp ( ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ↔ ( ( ( 𝐴𝑥 ) = 1o ∧ ( 𝐵𝑥 ) = ∅ ) ∨ ( ( 𝐴𝑥 ) = 1o ∧ ( 𝐵𝑥 ) = 2o ) ∨ ( ( 𝐴𝑥 ) = ∅ ∧ ( 𝐵𝑥 ) = 2o ) ) )
74 df-ne ( ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) ↔ ¬ ( 𝐴𝑥 ) = ( 𝐵𝑥 ) )
75 70 73 74 3imtr4i ( ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) → ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) )
76 fveq2 ( 𝑎 = 𝑥 → ( 𝐴𝑎 ) = ( 𝐴𝑥 ) )
77 fveq2 ( 𝑎 = 𝑥 → ( 𝐵𝑎 ) = ( 𝐵𝑥 ) )
78 76 77 neeq12d ( 𝑎 = 𝑥 → ( ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) ↔ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) ) )
79 78 elrab ( 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ↔ ( 𝑥 ∈ On ∧ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) ) )
80 79 biimpri ( ( 𝑥 ∈ On ∧ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) ) → 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
81 80 adantlr ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) ) → 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
82 ssrab2 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ⊆ On
83 ne0i ( 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ≠ ∅ )
84 83 adantl ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ≠ ∅ )
85 onint ( ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ⊆ On ∧ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ≠ ∅ ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
86 82 84 85 sylancr ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
87 nfrab1 𝑎 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) }
88 87 nfint 𝑎 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) }
89 nfcv 𝑎 On
90 nfcv 𝑎 𝐴
91 90 88 nffv 𝑎 ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
92 nfcv 𝑎 𝐵
93 92 88 nffv 𝑎 ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
94 91 93 nfne 𝑎 ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ≠ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
95 fveq2 ( 𝑎 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( 𝐴𝑎 ) = ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
96 fveq2 ( 𝑎 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( 𝐵𝑎 ) = ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
97 95 96 neeq12d ( 𝑎 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) ↔ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ≠ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
98 88 89 94 97 elrabf ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ↔ ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ≠ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
99 98 simprbi ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ≠ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
100 86 99 syl ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ≠ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
101 df-ne ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ≠ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ↔ ¬ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
102 100 101 sylib ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ¬ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
103 fveq2 ( 𝑦 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( 𝐴𝑦 ) = ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
104 fveq2 ( 𝑦 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( 𝐵𝑦 ) = ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
105 103 104 eqeq12d ( 𝑦 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ↔ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
106 105 rspccv ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) → ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ 𝑥 → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
107 106 ad2antlr ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ 𝑥 → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
108 102 107 mtod ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ¬ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ 𝑥 )
109 simpll ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → 𝑥 ∈ On )
110 oninton ( ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ⊆ On ∧ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ≠ ∅ ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On )
111 82 83 110 sylancr ( 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On )
112 111 adantl ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On )
113 ontri1 ( ( 𝑥 ∈ On ∧ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On ) → ( 𝑥 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ↔ ¬ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ 𝑥 ) )
114 109 112 113 syl2anc ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ( 𝑥 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ↔ ¬ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ 𝑥 ) )
115 108 114 mpbird ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → 𝑥 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
116 intss1 ( 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ⊆ 𝑥 )
117 116 adantl ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ⊆ 𝑥 )
118 115 117 eqssd ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
119 81 118 syldan ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) ) → 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
120 75 119 sylan2 ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) → 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
121 120 fveq2d ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) → ( 𝐴𝑥 ) = ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
122 120 fveq2d ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) → ( 𝐵𝑥 ) = ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
123 121 122 breq12d ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) → ( ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ↔ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
124 123 biimpd ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) → ( ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
125 124 ex ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) → ( ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) → ( ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ) )
126 125 pm2.43d ( ( 𝑥 ∈ On ∧ ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) → ( ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
127 126 expimpd ( 𝑥 ∈ On → ( ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
128 127 rexlimiv ( ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
129 50 128 impbid1 ( ( 𝐴 No 𝐵 No ) → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) ) )
130 1 129 bitr4d ( ( 𝐴 No 𝐵 No ) → ( 𝐴 <s 𝐵 ↔ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )