Metamath Proof Explorer


Theorem bnj1398

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 bnj1398.1 𝐵 = { 𝑑 ∣ ( 𝑑𝐴 ∧ ∀ 𝑥𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
bnj1398.2 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1398.3 𝐶 = { 𝑓 ∣ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) }
bnj1398.4 ( 𝜏 ↔ ( 𝑓𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
bnj1398.5 𝐷 = { 𝑥𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
bnj1398.6 ( 𝜓 ↔ ( 𝑅 FrSe 𝐴𝐷 ≠ ∅ ) )
bnj1398.7 ( 𝜒 ↔ ( 𝜓𝑥𝐷 ∧ ∀ 𝑦𝐷 ¬ 𝑦 𝑅 𝑥 ) )
bnj1398.8 ( 𝜏′[ 𝑦 / 𝑥 ] 𝜏 )
bnj1398.9 𝐻 = { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
bnj1398.10 𝑃 = 𝐻
bnj1398.11 ( 𝜃 ↔ ( 𝜒𝑧 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
bnj1398.12 ( 𝜂 ↔ ( 𝜃𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
Assertion bnj1398 ( 𝜒 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) = dom 𝑃 )

Proof

Step Hyp Ref Expression
1 bnj1398.1 𝐵 = { 𝑑 ∣ ( 𝑑𝐴 ∧ ∀ 𝑥𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1398.2 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1398.3 𝐶 = { 𝑓 ∣ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) }
4 bnj1398.4 ( 𝜏 ↔ ( 𝑓𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
5 bnj1398.5 𝐷 = { 𝑥𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
6 bnj1398.6 ( 𝜓 ↔ ( 𝑅 FrSe 𝐴𝐷 ≠ ∅ ) )
7 bnj1398.7 ( 𝜒 ↔ ( 𝜓𝑥𝐷 ∧ ∀ 𝑦𝐷 ¬ 𝑦 𝑅 𝑥 ) )
8 bnj1398.8 ( 𝜏′[ 𝑦 / 𝑥 ] 𝜏 )
9 bnj1398.9 𝐻 = { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
10 bnj1398.10 𝑃 = 𝐻
11 bnj1398.11 ( 𝜃 ↔ ( 𝜒𝑧 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
12 bnj1398.12 ( 𝜂 ↔ ( 𝜃𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
13 df-iun 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) = { 𝑧 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) }
14 13 bnj1436 ( 𝑧 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
15 11 14 simplbiim ( 𝜃 → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
16 nfv 𝑦 𝜓
17 nfv 𝑦 𝑥𝐷
18 nfra1 𝑦𝑦𝐷 ¬ 𝑦 𝑅 𝑥
19 16 17 18 nf3an 𝑦 ( 𝜓𝑥𝐷 ∧ ∀ 𝑦𝐷 ¬ 𝑦 𝑅 𝑥 )
20 7 19 nfxfr 𝑦 𝜒
21 nfiu1 𝑦 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
22 21 nfcri 𝑦 𝑧 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
23 20 22 nfan 𝑦 ( 𝜒𝑧 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
24 11 23 nfxfr 𝑦 𝜃
25 24 nf5ri ( 𝜃 → ∀ 𝑦 𝜃 )
26 15 12 25 bnj1521 ( 𝜃 → ∃ 𝑦 𝜂 )
27 nfv 𝑓 𝑅 FrSe 𝐴
28 nfe1 𝑓𝑓 𝜏
29 28 nfn 𝑓 ¬ ∃ 𝑓 𝜏
30 nfcv 𝑓 𝐴
31 29 30 nfrabw 𝑓 { 𝑥𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
32 5 31 nfcxfr 𝑓 𝐷
33 nfcv 𝑓
34 32 33 nfne 𝑓 𝐷 ≠ ∅
35 27 34 nfan 𝑓 ( 𝑅 FrSe 𝐴𝐷 ≠ ∅ )
36 6 35 nfxfr 𝑓 𝜓
37 32 nfcri 𝑓 𝑥𝐷
38 nfv 𝑓 ¬ 𝑦 𝑅 𝑥
39 32 38 nfralw 𝑓𝑦𝐷 ¬ 𝑦 𝑅 𝑥
40 36 37 39 nf3an 𝑓 ( 𝜓𝑥𝐷 ∧ ∀ 𝑦𝐷 ¬ 𝑦 𝑅 𝑥 )
41 7 40 nfxfr 𝑓 𝜒
42 nfv 𝑓 𝑧 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
43 41 42 nfan 𝑓 ( 𝜒𝑧 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
44 11 43 nfxfr 𝑓 𝜃
45 nfv 𝑓 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 )
46 nfv 𝑓 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
47 44 45 46 nf3an 𝑓 ( 𝜃𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
48 12 47 nfxfr 𝑓 𝜂
49 48 nf5ri ( 𝜂 → ∀ 𝑓 𝜂 )
50 11 simplbi ( 𝜃𝜒 )
51 12 50 bnj835 ( 𝜂𝜒 )
52 12 simp2bi ( 𝜂𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) )
53 1 2 3 4 5 6 7 8 bnj1388 ( 𝜒 → ∀ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∃ 𝑓 𝜏′ )
54 rsp ( ∀ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∃ 𝑓 𝜏′ → ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ∃ 𝑓 𝜏′ ) )
55 53 54 syl ( 𝜒 → ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ∃ 𝑓 𝜏′ ) )
56 51 52 55 sylc ( 𝜂 → ∃ 𝑓 𝜏′ )
57 49 56 bnj596 ( 𝜂 → ∃ 𝑓 ( 𝜂𝜏′ ) )
58 1 2 3 4 8 bnj1373 ( 𝜏′ ↔ ( 𝑓𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
59 58 simplbi ( 𝜏′𝑓𝐶 )
60 59 adantl ( ( 𝜂𝜏′ ) → 𝑓𝐶 )
61 58 simprbi ( 𝜏′ → dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
62 rspe ( ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
63 52 61 62 syl2an ( ( 𝜂𝜏′ ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
64 9 abeq2i ( 𝑓𝐻 ↔ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ )
65 58 rexbii ( ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ ↔ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑓𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
66 r19.42v ( ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑓𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑓𝐶 ∧ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
67 64 65 66 3bitri ( 𝑓𝐻 ↔ ( 𝑓𝐶 ∧ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
68 60 63 67 sylanbrc ( ( 𝜂𝜏′ ) → 𝑓𝐻 )
69 12 simp3bi ( 𝜂𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
70 69 adantr ( ( 𝜂𝜏′ ) → 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
71 61 adantl ( ( 𝜂𝜏′ ) → dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
72 70 71 eleqtrrd ( ( 𝜂𝜏′ ) → 𝑧 ∈ dom 𝑓 )
73 68 72 jca ( ( 𝜂𝜏′ ) → ( 𝑓𝐻𝑧 ∈ dom 𝑓 ) )
74 57 73 bnj593 ( 𝜂 → ∃ 𝑓 ( 𝑓𝐻𝑧 ∈ dom 𝑓 ) )
75 df-rex ( ∃ 𝑓𝐻 𝑧 ∈ dom 𝑓 ↔ ∃ 𝑓 ( 𝑓𝐻𝑧 ∈ dom 𝑓 ) )
76 74 75 sylibr ( 𝜂 → ∃ 𝑓𝐻 𝑧 ∈ dom 𝑓 )
77 10 dmeqi dom 𝑃 = dom 𝐻
78 9 bnj1317 ( 𝑤𝐻 → ∀ 𝑓 𝑤𝐻 )
79 78 bnj1400 dom 𝐻 = 𝑓𝐻 dom 𝑓
80 77 79 eqtri dom 𝑃 = 𝑓𝐻 dom 𝑓
81 80 eleq2i ( 𝑧 ∈ dom 𝑃𝑧 𝑓𝐻 dom 𝑓 )
82 eliun ( 𝑧 𝑓𝐻 dom 𝑓 ↔ ∃ 𝑓𝐻 𝑧 ∈ dom 𝑓 )
83 81 82 bitri ( 𝑧 ∈ dom 𝑃 ↔ ∃ 𝑓𝐻 𝑧 ∈ dom 𝑓 )
84 76 83 sylibr ( 𝜂𝑧 ∈ dom 𝑃 )
85 26 84 bnj593 ( 𝜃 → ∃ 𝑦 𝑧 ∈ dom 𝑃 )
86 nfre1 𝑦𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′
87 86 nfab 𝑦 { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
88 9 87 nfcxfr 𝑦 𝐻
89 88 nfuni 𝑦 𝐻
90 10 89 nfcxfr 𝑦 𝑃
91 90 nfdm 𝑦 dom 𝑃
92 91 nfcrii ( 𝑧 ∈ dom 𝑃 → ∀ 𝑦 𝑧 ∈ dom 𝑃 )
93 85 92 bnj1397 ( 𝜃𝑧 ∈ dom 𝑃 )
94 11 93 sylbir ( ( 𝜒𝑧 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → 𝑧 ∈ dom 𝑃 )
95 94 ex ( 𝜒 → ( 𝑧 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ dom 𝑃 ) )
96 95 ssrdv ( 𝜒 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ⊆ dom 𝑃 )
97 simpr ( ( 𝑓𝐻𝑧 ∈ dom 𝑓 ) → 𝑧 ∈ dom 𝑓 )
98 67 simprbi ( 𝑓𝐻 → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
99 98 adantr ( ( 𝑓𝐻𝑧 ∈ dom 𝑓 ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
100 r19.42v ( ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑧 ∈ dom 𝑓 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑧 ∈ dom 𝑓 ∧ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
101 eleq2 ( dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → ( 𝑧 ∈ dom 𝑓𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
102 101 biimpac ( ( 𝑧 ∈ dom 𝑓 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
103 102 reximi ( ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑧 ∈ dom 𝑓 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
104 100 103 sylbir ( ( 𝑧 ∈ dom 𝑓 ∧ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
105 97 99 104 syl2anc ( ( 𝑓𝐻𝑧 ∈ dom 𝑓 ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
106 105 rexlimiva ( ∃ 𝑓𝐻 𝑧 ∈ dom 𝑓 → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
107 eliun ( 𝑧 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
108 106 83 107 3imtr4i ( 𝑧 ∈ dom 𝑃𝑧 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
109 108 ssriv dom 𝑃 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
110 109 a1i ( 𝜒 → dom 𝑃 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
111 96 110 eqssd ( 𝜒 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) = dom 𝑃 )