Metamath Proof Explorer

Theorem bnj1311

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1311.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
bnj1311.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1311.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
bnj1311.4 ⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
Assertion bnj1311 ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ) → ( 𝑔 ↾ 𝐷 ) = ( ℎ ↾ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 bnj1311.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1311.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1311.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4 bnj1311.4 ⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
5 biid ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
6 5 bnj1232 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) → 𝑅 FrSe 𝐴 )
7 ssrab2 ⊢ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ⊆ 𝐷
8 5 bnj1235 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) → 𝑔 ∈ 𝐶 )
9 eqid ⊢ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
10 eqid ⊢ { 𝑔 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) } = { 𝑔 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) }
11 2 3 9 10 bnj1234 ⊢ 𝐶 = { 𝑔 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) }
12 8 11 eleqtrdi ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) → 𝑔 ∈ { 𝑔 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) } )
13 abid ⊢ ( 𝑔 ∈ { 𝑔 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) } ↔ ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
14 13 bnj1238 ⊢ ( 𝑔 ∈ { 𝑔 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) } → ∃ 𝑑 ∈ 𝐵 𝑔 Fn 𝑑 )
15 14 bnj1196 ⊢ ( 𝑔 ∈ { 𝑔 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) } → ∃ 𝑑 ( 𝑑 ∈ 𝐵 ∧ 𝑔 Fn 𝑑 ) )
16 1 eqabri ⊢ ( 𝑑 ∈ 𝐵 ↔ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
17 16 simplbi ⊢ ( 𝑑 ∈ 𝐵 → 𝑑 ⊆ 𝐴 )
18 fndm ⊢ ( 𝑔 Fn 𝑑 → dom 𝑔 = 𝑑 )
19 17 18 bnj1241 ⊢ ( ( 𝑑 ∈ 𝐵 ∧ 𝑔 Fn 𝑑 ) → dom 𝑔 ⊆ 𝐴 )
20 15 19 bnj593 ⊢ ( 𝑔 ∈ { 𝑔 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) } → ∃ 𝑑 dom 𝑔 ⊆ 𝐴 )
21 20 bnj937 ⊢ ( 𝑔 ∈ { 𝑔 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) } → dom 𝑔 ⊆ 𝐴 )
22 ssinss1 ⊢ ( dom 𝑔 ⊆ 𝐴 → ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 )
23 12 21 22 3syl ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) → ( dom 𝑔 ∩ dom ℎ ) ⊆ 𝐴 )
24 4 23 eqsstrid ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) → 𝐷 ⊆ 𝐴 )
25 7 24 sstrid ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) → { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ⊆ 𝐴 )
26 eqid ⊢ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
27 biid ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ¬ 𝑦 𝑅 𝑥 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ¬ 𝑦 𝑅 𝑥 ) )
28 1 2 3 4 26 5 27 bnj1253 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) → { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ≠ ∅ )
29 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
30 29 nfcrii ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } → ∀ 𝑥 𝑧 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } )
31 30 bnj1228 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ⊆ 𝐴 ∧ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ≠ ∅ ) → ∃ 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ∀ 𝑦 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ¬ 𝑦 𝑅 𝑥 )
32 6 25 28 31 syl3anc ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) → ∃ 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ∀ 𝑦 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ¬ 𝑦 𝑅 𝑥 )
33 ax-5 ⊢ ( 𝑅 FrSe 𝐴 → ∀ 𝑥 𝑅 FrSe 𝐴 )
34 1 bnj1309 ⊢ ( 𝑤 ∈ 𝐵 → ∀ 𝑥 𝑤 ∈ 𝐵 )
35 3 34 bnj1307 ⊢ ( 𝑤 ∈ 𝐶 → ∀ 𝑥 𝑤 ∈ 𝐶 )
36 35 hblem ⊢ ( 𝑔 ∈ 𝐶 → ∀ 𝑥 𝑔 ∈ 𝐶 )
37 35 hblem ⊢ ( ℎ ∈ 𝐶 → ∀ 𝑥 ℎ ∈ 𝐶 )
38 ax-5 ⊢ ( ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) → ∀ 𝑥 ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) )
39 33 36 37 38 bnj982 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) → ∀ 𝑥 ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
40 32 27 39 bnj1521 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) → ∃ 𝑥 ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ¬ 𝑦 𝑅 𝑥 ) )
41 simp2 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ¬ 𝑦 𝑅 𝑥 ) → 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } )
42 1 2 3 4 26 5 27 bnj1279 ⊢ ( ( 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ¬ 𝑦 𝑅 𝑥 ) → ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ) = ∅ )
43 42 3adant1 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ¬ 𝑦 𝑅 𝑥 ) → ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ) = ∅ )
44 1 2 3 4 26 5 27 43 bnj1280 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ¬ 𝑦 𝑅 𝑥 ) → ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) )
45 eqid ⊢ ⟨ 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
46 eqid ⊢ { ℎ ∣ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) } = { ℎ ∣ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) }
47 1 2 3 4 26 5 27 44 9 10 45 46 bnj1296 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ¬ 𝑦 𝑅 𝑥 ) → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) )
48 26 bnj1538 ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } → ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) )
49 48 necon2bi ⊢ ( ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) → ¬ 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } )
50 47 49 syl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ¬ 𝑦 𝑅 𝑥 ) → ¬ 𝑥 ∈ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } )
51 40 41 50 bnj1304 ⊢ ¬ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) )
52 df-bnj17 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ) ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
53 51 52 mtbi ⊢ ¬ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ) ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) )
54 53 imnani ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ) → ¬ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) )
55 nne ⊢ ( ¬ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ↔ ( 𝑔 ↾ 𝐷 ) = ( ℎ ↾ 𝐷 ) )
56 54 55 sylib ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ) → ( 𝑔 ↾ 𝐷 ) = ( ℎ ↾ 𝐷 ) )