Theorem bnj1523

Description: Technical lemma for bnj1522 . 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	bnj1523.1	⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
	bnj1523.2	⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
	bnj1523.3	⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
	bnj1523.4	⊢ 𝐹 = ∪ 𝐶
	bnj1523.5	⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
	bnj1523.6	⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) )
	bnj1523.7	⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) ) )
	bnj1523.8	⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) }
	bnj1523.9	⊢ ( 𝜃 ↔ ( 𝜒 ∧ 𝑦 ∈ 𝐷 ∧ ∀ 𝑧 ∈ 𝐷 ¬ 𝑧 𝑅 𝑦 ) )
Assertion	bnj1523	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) → 𝐹 = 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		bnj1523.1	⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2		bnj1523.2	⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3		bnj1523.3	⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4		bnj1523.4	⊢ 𝐹 = ∪ 𝐶
5		bnj1523.5	⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
6		bnj1523.6	⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) )
7		bnj1523.7	⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) ) )
8		bnj1523.8	⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) }
9		bnj1523.9	⊢ ( 𝜃 ↔ ( 𝜒 ∧ 𝑦 ∈ 𝐷 ∧ ∀ 𝑧 ∈ 𝐷 ¬ 𝑧 𝑅 𝑦 ) )
10	1 2 3 4	bnj60	⊢ ( 𝑅 FrSe 𝐴 → 𝐹 Fn 𝐴 )
11	5 10	bnj835	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
12	6 11	bnj832	⊢ ( 𝜓 → 𝐹 Fn 𝐴 )
13	7 12	bnj835	⊢ ( 𝜒 → 𝐹 Fn 𝐴 )
14	9 13	bnj835	⊢ ( 𝜃 → 𝐹 Fn 𝐴 )
15	5	simp2bi	⊢ ( 𝜑 → 𝐻 Fn 𝐴 )
16	6 15	bnj832	⊢ ( 𝜓 → 𝐻 Fn 𝐴 )
17	7 16	bnj835	⊢ ( 𝜒 → 𝐻 Fn 𝐴 )
18	9 17	bnj835	⊢ ( 𝜃 → 𝐻 Fn 𝐴 )
19		bnj213	⊢ pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
20	19	a1i	⊢ ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴 )
21	9	simp3bi	⊢ ( 𝜃 → ∀ 𝑧 ∈ 𝐷 ¬ 𝑧 𝑅 𝑦 )
22	21	bnj1211	⊢ ( 𝜃 → ∀ 𝑧 ( 𝑧 ∈ 𝐷 → ¬ 𝑧 𝑅 𝑦 ) )
23		con2b	⊢ ( ( 𝑧 ∈ 𝐷 → ¬ 𝑧 𝑅 𝑦 ) ↔ ( 𝑧 𝑅 𝑦 → ¬ 𝑧 ∈ 𝐷 ) )
24	23	albii	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝐷 → ¬ 𝑧 𝑅 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 𝑅 𝑦 → ¬ 𝑧 ∈ 𝐷 ) )
25	22 24	sylib	⊢ ( 𝜃 → ∀ 𝑧 ( 𝑧 𝑅 𝑦 → ¬ 𝑧 ∈ 𝐷 ) )
26		bnj1418	⊢ ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 𝑅 𝑦 )
27	26	imim1i	⊢ ( ( 𝑧 𝑅 𝑦 → ¬ 𝑧 ∈ 𝐷 ) → ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → ¬ 𝑧 ∈ 𝐷 ) )
28	27	alimi	⊢ ( ∀ 𝑧 ( 𝑧 𝑅 𝑦 → ¬ 𝑧 ∈ 𝐷 ) → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → ¬ 𝑧 ∈ 𝐷 ) )
29	25 28	syl	⊢ ( 𝜃 → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → ¬ 𝑧 ∈ 𝐷 ) )
30	29	ralrid	⊢ ( 𝜃 → ∀ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ¬ 𝑧 ∈ 𝐷 )
31	1	bnj1309	⊢ ( 𝑤 ∈ 𝐵 → ∀ 𝑥 𝑤 ∈ 𝐵 )
32	3 31	bnj1307	⊢ ( 𝑤 ∈ 𝐶 → ∀ 𝑥 𝑤 ∈ 𝐶 )
33	32	nfcii	⊢ Ⅎ 𝑥 𝐶
34	33	nfuni	⊢ Ⅎ 𝑥 ∪ 𝐶
35	4 34	nfcxfr	⊢ Ⅎ 𝑥 𝐹
36	35	nfcrii	⊢ ( 𝑤 ∈ 𝐹 → ∀ 𝑥 𝑤 ∈ 𝐹 )
37	8 36	bnj1534	⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐻 ‘ 𝑧 ) }
38	30 19 37	bnj1533	⊢ ( 𝜃 → ∀ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ 𝑧 ) )
39	14 18 20 38	bnj1536	⊢ ( 𝜃 → ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) = ( 𝐻 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
40	39	opeq2d	⊢ ( 𝜃 → ⟨ 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑦 , ( 𝐻 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ )
41	40	fveq2d	⊢ ( 𝜃 → ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐻 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
42	1 2 3 4	bnj1500	⊢ ( 𝑅 FrSe 𝐴 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
43	5 42	bnj835	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
44	6 43	bnj832	⊢ ( 𝜓 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
45	7 44	bnj835	⊢ ( 𝜒 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
46	45 36	bnj1529	⊢ ( 𝜒 → ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
47	9 46	bnj835	⊢ ( 𝜃 → ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
48	8	ssrab3	⊢ 𝐷 ⊆ 𝐴
49	9	simp2bi	⊢ ( 𝜃 → 𝑦 ∈ 𝐷 )
50	48 49	bnj1213	⊢ ( 𝜃 → 𝑦 ∈ 𝐴 )
51	47 50	bnj1294	⊢ ( 𝜃 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
52	5	simp3bi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
53	6 52	bnj832	⊢ ( 𝜓 → ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
54	7 53	bnj835	⊢ ( 𝜒 → ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
55		ax-5	⊢ ( 𝑣 ∈ 𝐻 → ∀ 𝑥 𝑣 ∈ 𝐻 )
56	54 55	bnj1529	⊢ ( 𝜒 → ∀ 𝑦 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐻 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
57	9 56	bnj835	⊢ ( 𝜃 → ∀ 𝑦 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐻 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
58	57 50	bnj1294	⊢ ( 𝜃 → ( 𝐻 ‘ 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐻 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
59	41 51 58	3eqtr4d	⊢ ( 𝜃 → ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) )
60	8 36	bnj1534	⊢ 𝐷 = { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐻 ‘ 𝑦 ) }
61	60	bnj1538	⊢ ( 𝑦 ∈ 𝐷 → ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐻 ‘ 𝑦 ) )
62	9 61	bnj836	⊢ ( 𝜃 → ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐻 ‘ 𝑦 ) )
63	62	neneqd	⊢ ( 𝜃 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) )
64	59 63	pm2.65i	⊢ ¬ 𝜃
65	64	nex	⊢ ¬ ∃ 𝑦 𝜃
66	5	simp1bi	⊢ ( 𝜑 → 𝑅 FrSe 𝐴 )
67	6 66	bnj832	⊢ ( 𝜓 → 𝑅 FrSe 𝐴 )
68	7 67	bnj835	⊢ ( 𝜒 → 𝑅 FrSe 𝐴 )
69	48	a1i	⊢ ( 𝜒 → 𝐷 ⊆ 𝐴 )
70	7	simp2bi	⊢ ( 𝜒 → 𝑥 ∈ 𝐴 )
71	7	simp3bi	⊢ ( 𝜒 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) )
72	8	reqabi	⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) ) )
73	70 71 72	sylanbrc	⊢ ( 𝜒 → 𝑥 ∈ 𝐷 )
74	73	ne0d	⊢ ( 𝜒 → 𝐷 ≠ ∅ )
75		bnj69	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ 𝐷 ≠ ∅ ) → ∃ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝐷 ¬ 𝑧 𝑅 𝑦 )
76	68 69 74 75	syl3anc	⊢ ( 𝜒 → ∃ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝐷 ¬ 𝑧 𝑅 𝑦 )
77	76 9	bnj1209	⊢ ( 𝜒 → ∃ 𝑦 𝜃 )
78	65 77	mto	⊢ ¬ 𝜒
79	78	nex	⊢ ¬ ∃ 𝑥 𝜒
80	6	simprbi	⊢ ( 𝜓 → 𝐹 ≠ 𝐻 )
81	12 16 80 36	bnj1542	⊢ ( 𝜓 → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) )
82	1 2 3 4 5 6	bnj1525	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
83	81 7 82	bnj1521	⊢ ( 𝜓 → ∃ 𝑥 𝜒 )
84	79 83	mto	⊢ ¬ 𝜓
85	6 84	bnj1541	⊢ ( 𝜑 → 𝐹 = 𝐻 )
86	5 85	sylbir	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) → 𝐹 = 𝐻 )